OAI/NumberTheory/TwoPoint/Walks/TupleRankCoordinate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the selected rank estimate to one literal outside-coordinate fiber.

  1. theorem OAI.TwoPointCorrelations.tuple_rank_coordinate_sum line 13