ofZLatticeComap_repr_apply — Mathlib

English

The coordinates of the comap-basis with respect to the image of e under the repr agree with the original repr.

Русский

Координаты базы, полученной через comap, в представлении совпадают с исходными координатами.

LaTeX

$$$(\\text{Basis.ofZLatticeComap } K L e)\\mathrm{repr}(ZLattice.comap_equiv K L e x) i = (\\text{Basis}.repr\\; x) i$$$

Lean4

@[simp]
theorem ofZLatticeComap_repr_apply (e : F ≃ₗ[K] E) {ι : Type*} (b : Basis ι ℤ L) (x : L) (i : ι) :
    (b.ofZLatticeComap K L e).repr (ZLattice.comap_equiv K L e x) i = b.repr x i := by simp [Basis.ofZLatticeComap]

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