span_idealLatticeBasis — Mathlib

English

The span of the ideal lattice basis equals the ideal lattice in the mixed embedding.

Русский

Область спана базиса идеальной решётки совпадает с идеальной решёткой в смешанном вложении.

LaTeX

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

Lean4

theorem span_idealLatticeBasis :
    (Submodule.span ℤ (Set.range (fractionalIdealLatticeBasis K I))) = (mixedEmbedding.idealLattice K I) :=
  by
  ext x
  simp [mem_span_fractionalIdealLatticeBasis]

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