ofZLatticeBasis_span — Mathlib

English

The Z-span of the constructed basis equals the lattice L.

Русский

Z-область (span) построенного базиса равна самой решётке L.

LaTeX

$$$\\operatorname{span}_{\\mathbb{Z}}(\\{b_i : i\\in \\iota\\}) = L$$$

Lean4

theorem ofZLatticeBasis_span : span ℤ (Set.range (b.ofZLatticeBasis K)) = L := by
  calc
    span ℤ (Set.range (b.ofZLatticeBasis K))
    _ = span ℤ (L.subtype '' Set.range b) := by congr; ext; simp
    _ = map L.subtype (span ℤ (Set.range b)) := by rw [Submodule.map_span]
    _ = L := by simp [b.span_eq]

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