ofZLatticeBasis_comap — Mathlib

English

The base change is compatible with comap, i.e., comap of a basis equals the mapped basis.

Русский

Переход баз через comap совместим с отображением основы: comap базы равен образующей базы.

LaTeX

$$$\\text{Basis.ofZLatticeComap}(K,L,e) = \\text{Basis}.map( e^{-1})$$$

Lean4

theorem ofZLatticeBasis_comap (e : F ≃L[K] E) {ι : Type*} (b : Basis ι ℤ L) :
    (b.ofZLatticeComap K L e.toLinearEquiv).ofZLatticeBasis K (ZLattice.comap K L e.toLinearMap) =
      (b.ofZLatticeBasis K L).map e.symm.toLinearEquiv :=
  by
  ext
  simp

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