Commit 2025-08-11 22:54 38273974

View on Github →

feat(ZLattice/Covolume): add covolume_div_covolume_eq_relindex (#25730) Add the following result: Let L₁ be a sub-ℤ-lattice of L₂. Then the index of L₁ inside L₂ is equal to covolume L₁ / covolume L₂.

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

added def IsZLattice.basis

added theorem ZLattice.comap_toAddSubgroup

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

added theorem ZLattice.covolume_div_covolume_eq_relindex'

added theorem ZLattice.covolume_div_covolume_eq_relindex

modified theorem ZLattice.volume_image_eq_volume_div_covolume

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.relindex_map_map_of_injective

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Module.Basis.det_mul_det