ℤ-Linear Equivalences of Lattices with ℤ^n.

In this file, we prove that there is a ℤ-linear equivalence of any lattice in Euclidean Space with the standard lattice ℤ^n (as defined in SpherePacking.ForMathlib.PoissonSummation.Zn_Pi).

noncomputable def ZLattice.equiv_Zn {n : ℕ} (Λ : Submodule ℤ (Fin n → ℝ)) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] : ↥Λ ≃ₗ[ℤ] ↥(ℤ^n)

Any lattice in Euclidean space is ℤ-linearly equivalent to ↑ℤ^n.

Equations

• ZLattice.equiv_Zn Λ = LinearEquiv.ofFinrankEq ↥Λ ↥(ℤ^n) ⋯

noncomputable def ZLattice.Zn_equiv {n : ℕ} (Λ : Submodule ℤ (Fin n → ℝ)) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] : ↥(ℤ^n) ≃ₗ[ℤ] ↥Λ

For any ZLattice Λ in ℝ^n, the LinearEquiv from ℤ^n to Λ.

Equations

• ZLattice.Zn_equiv Λ = (ZLattice.equiv_Zn Λ).symm