basisOfBasisRight_apply — Mathlib

English

If H encodes a linear disjointness between A and B, then the basis obtained on the right maps under the natural algebra map to the expected coordinates.

Русский

Пусть H кодирует линейную разобщенность между A и B; базис справа переходит через естественное алгебраическое отображение в ожидаемые координаты.

LaTeX

$$$H.basisOfBasisRight H' b \; i = \text{algebraMap}_{B E}(b(i))$$$

Lean4

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

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