Commit 2023-06-09 16:56 f6846618

View on Github →

feat: port MeasureTheory.Group.GeometryOfNumbers (#4915)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

added theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure

added theorem MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd