basisOfBasisLeft_apply — Mathlib

English

The i-th element of the left basis equals the image of b_i under the inclusion A → S.

Русский

i-й элемент базиса слева равен образу b_i при включении A в S.

LaTeX

$$$H.basisOfBasisLeft H' b i = algebraMap A S (b i)$$$

Lean4

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

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