comap_span_top — Mathlib

English

If e is a linear equivalence, then there is a ℤ-linear equivalence between L and ZLattice.comap K L e.

Русский

Если e — линейное эквивалентность, существует ℤ-линейное эквивалентное отображение между L и ZLattice.comap K L e.

LaTeX

$$$L \\cong_{\\mathbb{Z}} ZLattice.comap K L e$$$

Lean4

theorem comap_span_top (hL : span K (L : Set E) = ⊤) {e : F →ₗ[K] E} (he : (L : Set E) ⊆ LinearMap.range e) :
    span K (ZLattice.comap K L e : Set F) = ⊤ := by
  rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]

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