noncomputable def LatticeBasics.lattice (n m : ℕ) (b : Fin n → Fin m → ℝ) (_hli : LinearIndependent ℝ b) : Submodule ℤ (Fin m → ℝ)

def LatticeBasics.IsUnimodular {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℤ) : Prop

theorem LatticeBasics.isUnimodular_iff_isUnit_det {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℤ) : IsUnimodular U ↔ IsUnit U.det

theorem LatticeBasics.isUnimodular_inv {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℤ) (hU : IsUnimodular U) : IsUnimodular U⁻¹

theorem LatticeBasics.isUnimodular_inv_iff {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℤ) : IsUnimodular U ↔ IsUnimodular U⁻¹

def LatticeBasics.dualLattice {m : ℕ} (L : Submodule ℤ (Fin m → ℝ)) : Submodule ℤ (Fin m → ℝ)

def LatticeBasics.IsDualBasis {n m : ℕ} (b b' : Fin n → Fin m → ℝ) : Prop

theorem LatticeBasics.equivalent_bases_iff (n m : ℕ) (b₁ b₂ : Fin n → Fin m → ℝ) (hli₁ : LinearIndependent ℝ b₁) (hli₂ : LinearIndependent ℝ b₂) : lattice n m b₁ hli₁ = lattice n m b₂ hli₂ ↔ ∃ (U : Matrix (Fin n) (Fin n) ℤ), IsUnimodular U ∧ ∀ (j : Fin n), b₂ j = ∑ i : Fin n, U i j • b₁ i

def LatticeBasics.fundamentalParallelepiped (n m : ℕ) (b : Fin n → Fin m → ℝ) : Set (Fin m → ℝ)

inductive LatticeBasics.IntColumnOp (n m : ℕ) : (Fin n → Fin m → ℝ) → (Fin n → Fin m → ℝ) → Prop

• addMultiple {n m : ℕ} (b : Fin n → Fin m → ℝ) (i j : Fin n) (hij : i ≠ j) (k : ℤ) : IntColumnOp n m b (Function.update b i (b i + k • b j))
• swap {n m : ℕ} (b : Fin n → Fin m → ℝ) (i j : Fin n) : IntColumnOp n m b (b ∘ ⇑(Equiv.swap i j))
• negate {n m : ℕ} (b : Fin n → Fin m → ℝ) (i : Fin n) : IntColumnOp n m b (Function.update b i (-b i))

inductive LatticeBasics.IntColumnOps (n m : ℕ) : (Fin n → Fin m → ℝ) → (Fin n → Fin m → ℝ) → Prop

• refl {n m : ℕ} (b : Fin n → Fin m → ℝ) : IntColumnOps n m b b
• step {n m : ℕ} {b₁ b₂ b₃ : Fin n → Fin m → ℝ} : IntColumnOps n m b₁ b₂ → IntColumnOp n m b₂ b₃ → IntColumnOps n m b₁ b₃

theorem LatticeBasics.equivalent_bases_column_ops (n m : ℕ) (b₁ b₂ : Fin n → Fin m → ℝ) (hli₁ : LinearIndependent ℝ b₁) (hli₂ : LinearIndependent ℝ b₂) : lattice n m b₁ hli₁ = lattice n m b₂ hli₂ ↔ IntColumnOps n m b₁ b₂

noncomputable def LatticeBasics.latticeDet (n m : ℕ) (b : Fin n → Fin m → ℝ) : ℝ

theorem LatticeBasics.latticeDet_eq_abs_det (n : ℕ) (b : Fin n → Fin n → ℝ) (_hli : LinearIndependent ℝ b) : latticeDet n n b = |(Matrix.of b).det|

theorem LatticeBasics.basis_iff_fundamentalParallelepiped_inter (n : ℕ) (b : Fin n → Fin n → ℝ) (hli : LinearIndependent ℝ b) (Λ : Submodule ℤ (Fin n → ℝ)) (hBinΛ : ∀ (i : Fin n), b i ∈ Λ) : lattice n n b hli = Λ ↔ fundamentalParallelepiped n n b ∩ ↑Λ = {0}

theorem LatticeBasics.blichfeldt (n : ℕ) [NeZero n] (b : Fin n → Fin n → ℝ) (hli : LinearIndependent ℝ b) (S : Set (Fin n → ℝ)) (hS : MeasurableSet S) (hvol : ENNReal.ofReal (latticeDet n n b) < MeasureTheory.volume S) : ∃ (z₁ : Fin n → ℝ) (z₂ : Fin n → ℝ), z₁ ∈ S ∧ z₂ ∈ S ∧ z₁ ≠ z₂ ∧ z₁ - z₂ ∈ lattice n n b hli

noncomputable def LatticeBasics.successiveMinimum (m : ℕ) (L : Submodule ℤ (Fin m → ℝ)) (i : ℕ) : ℝ