basisOfBasisLeft_repr_apply — Mathlib

English

Coordinates of the left basis under the representation equal those under the right algebra map.

Русский

Координаты базиса слева в представлении равны координатам под соответствующим алгебраическим отображением.

LaTeX

$$$(H.basisOfBasisLeft H' b).repr x i = (algebraMap (Subtype...) )$$$

Lean4

theorem basisOfBasisLeft_repr_apply (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*}
    (b : Basis ι F A) (x : A) (i : ι) :
    algebraMap B E ((H.basisOfBasisLeft H' b).repr x i) = algebraMap F E (b.repr x i) :=
  (linearDisjoint_iff'.mp H).basisOfBasisLeft_repr_apply H' b x i

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