ofZLatticeComap — Mathlib

English

The basis of ZLattice.comap K L e is given by the image of a basis b of L under e.symm.

Русский

База ZLattice.comap K L e задаётся образом базы b решётки L под e.symm.

LaTeX

$$$\\text{ofZLatticeComap}(K,L,e) = b.map( ZLattice.comap_equiv K L e)$$$

Lean4

/-- The basis of `ZLattice.comap K L e` given by the image of a basis `b` of `L` by `e.symm`. -/
def ofZLatticeComap (e : F ≃ₗ[K] E) {ι : Type*} (b : Basis ι ℤ L) : Basis ι ℤ (ZLattice.comap K L e.toLinearMap) :=
  b.map (ZLattice.comap_equiv K L e)

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