basisOfBasisLeft_repr_apply — Mathlib

English

For x in A, the A-algebra map applied to the i-th coordinate of the basisLeft repr equals the R-algebra map applied to the i-th coordinate of b.repr.

Русский

Пусть x ∈ A. Применение A-переображения к i-му коэффициенту представления basisLeft даёт координату, полученную через b.repr.

LaTeX

$$$\\mathrm{algebraMap}_{B\\to S}(((H.basisOfBasisLeft H' b).repr x i)) = \\mathrm{algebraMap}_{R\\to S}(b.repr x i)$$$

Lean4

theorem basisOfBasisLeft_repr_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R A) (x : A) (i : ι) :
    algebraMap B S ((H.basisOfBasisLeft H' b).repr x i) = algebraMap R S (b.repr x i) :=
  H.symm.algebraMap_basisOfBasisRight_repr_apply (by rwa [sup_comm]) b x i

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