basisOfBasisLeft_apply — Mathlib

English

The left basis maps to the algebra map coordinate on E.

Русский

Лево-образующий базис отображается в координаты через алгебраическое отображение в E.

LaTeX

$$$H.basisOfBasisLeft H' b i = algebraMap_{A E}( b(i) )$$$

Lean4

@[simp]
theorem basisOfBasisLeft_apply (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*}
    (b : Basis ι F A) (i : ι) : H.basisOfBasisLeft H' b i = algebraMap A E (b i) :=
  (linearDisjoint_iff'.mp H).basisOfBasisLeft_apply H' b i

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