algebraMap_basisOfBasisRight_apply

English

For each i, the i-th basis vector equals the image of b_i under the inclusion B → S.

Русский

Для каждого индекса i i-й элемент базиса равен образу b_i при включении B в S.

LaTeX

$$$H.basisOfBasisRight H' b i = (\\mathrm{algebraMap}_{B \\to S})(b_i)$$$

Lean4

@[simp]
theorem algebraMap_basisOfBasisRight_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B) (i : ι) :
    H.basisOfBasisRight H' b i = algebraMap B S (b i) := by simp [basisOfBasisRight]

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