algebraMap_basisOfBasisRight_repr_apply

English

The A-algebra map applied to the i-th coefficient from the basisRight repr equals the R-algebra map applied to the i-th coefficient from b.repr.

Русский

Применение A-переобразования к i-му коэффициенту представления basisRight даёт то же, что и применение R-алгебра-переобразования к i-му коэффициенту представления b.

LaTeX

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

Lean4

theorem algebraMap_basisOfBasisRight_repr_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B) (x : B) (i : ι) :
    algebraMap A S ((H.basisOfBasisRight H' b).repr x i) = algebraMap R S (b.repr x i) := by
  simp [basisOfBasisRight, Algebra.algebraMap_eq_smul_one]

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