Commit 2024-12-18 15:53 211dc533

View on Github →

feat (Lattice/Covolume): Add results linking point counting in lattices and covolume (#12488)

Estimated changes

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

added theorem Basis.ofZLatticeBasis_comap

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

added theorem ZLattice.covolume.tendsto_card_div_pow''

added theorem ZLattice.covolume.tendsto_card_div_pow'

added theorem ZLattice.covolume.tendsto_card_div_pow

added theorem ZLattice.covolume.tendsto_card_le_div''

added theorem ZLattice.covolume.tendsto_card_le_div'

added theorem ZLattice.covolume.tendsto_card_le_div

added theorem ZLattice.covolume_eq_det_inv

added theorem ZLattice.volume_image_eq_volume_div_covolume'

added theorem ZLattice.volume_image_eq_volume_div_covolume

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Basis.det_basis

added theorem Basis.det_inv

added theorem Pi.basisFun_det_apply