mem_span_latticeBasis — Mathlib

English

The span of the latticeBasis (over integers) coincides with the integer lattice of the mixed space.

Русский

Замыкание latticeBasis по целым числам совпадает с целочисленной решёткой смешанного пространства.

LaTeX

$$$ span\ Int (Set.range (latticeBasis K)) = mixedEmbedding.integerLattice K $$$

Lean4

theorem mem_span_latticeBasis {x : (mixedSpace K)} :
    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ mixedEmbedding.integerLattice K :=
  by
  rw [show Set.range (latticeBasis K) = (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
      rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
  rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
  simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K, RingHom.mem_range, exists_exists_eq_and]
  rfl

Похожие утверждения