mk_algebraMap — Mathlib

English

If r ∈ R maps into S via the algebra map, the image in S obtained from R matches the image of r in A, under the respective algebra maps.

Русский

Если r ∈ R отображается в S через алгебраическую карту, тогда образ в S совпадает с образом в A через соответствующие алгебраические отображения.

LaTeX

$$$\langle \mathrm{algebraMap}_{R,A}(r), hr\rangle = \mathrm{algebraMap}_{R,S}(r)$, hence $\mathrm{algebraMap}_{R,S}(r) = \mathrm{algebraMap}_{R,A}(r)$ in S.$$

Lean4

@[simp]
theorem mk_algebraMap {S : Subalgebra R A} (r : R) (hr : algebraMap R A r ∈ S) :
    ⟨algebraMap R A r, hr⟩ = algebraMap R S r :=
  rfl

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