algebraMap_def — Mathlib

English

For s in S, the image under algebraMap_Sα equals the image under algebraMap_Aα of the underlying A-element.

Русский

Для s ∈ S образ под алгебраического отображения algebraMap_Sα равен образу под algebraMap_Aα от соответствующего элемента A.

LaTeX

$$$\mathrm{algebraMap}_S^{\alpha}(s) = \mathrm{algebraMap}_A^{\alpha}(s:A)$$$

Lean4

theorem algebraMap_def {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α]
    {S : Subalgebra R A} (s : S) : algebraMap S α s = algebraMap A α (s : A) :=
  rfl

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