algebraMap_eq — Mathlib

English

The two algebra maps from S to α coincide with the composition of the inclusion S → A followed by the A-algebra map to α, i.e., algebraMap_Sα = algebraMap_Aα ∘ S.val.

Русский

Два отображения алгебры из S в α совпадают и равны композиции включения S → A с алгебраическим отображением A → α: algebraMap_Sα = algebraMap_Aα ∘ S.val.

LaTeX

$$$\mathrm{algebraMap}_S^{\alpha} = (\mathrm{algebraMap}_A^{\alpha}) \circ S.val$$$

Lean4

theorem algebraMap_eq {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α]
    (S : Subalgebra R A) : algebraMap S α = (algebraMap A α).comp S.val :=
  rfl

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