OAI/NumberTheory/Ostmann/Tree/UniformCoordinateAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinate marginals of the finite uniform CRT product

  1. theorem OAI.Ostmann.uniform_pi_coordinate_average line 11