algebraMap_mk — Mathlib

English

If a ∈ A and ha is a witness that a ∈ S, then algebraMap_Sα (⟨a, ha⟩) = algebraMap_Aα a.

Русский

Если a ∈ A и ha является доказательством того, что a ∈ S, то algebraMap_Sα (⟨a, ha⟩) = algebraMap_Aα a.

LaTeX

$$$\mathrm{algebraMap}_S^{\alpha}(\langle a, ha \rangle) = \mathrm{algebraMap}_A^{\alpha}(a)$$$

Lean4

@[simp]
theorem algebraMap_mk {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α]
    {S : Subalgebra R A} (a : A) (ha : a ∈ S) : algebraMap S α (⟨a, ha⟩ : S) = algebraMap A α a :=
  rfl

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