toAlgHom_toRingHom — Mathlib

English

The two ways of viewing an algebra equivalence as a RingHom give the same RingHom; the path through AlgHom and the path through RingEquiv agree.

Русский

Два способа рассмотреть алгебраическую эквивалентность как кольцевой гомоморфизм дают один и тот же RingHom; оба пути согласованы.

LaTeX

$$$ (e: A_1 \to_{R} A_2)^{\text{AlgHom}} = (e: A_1 \to_{+*} A_2)^{\text{RingHom}} $$$

Lean4

@[simp, norm_cast]
theorem toAlgHom_toRingHom : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = e :=
  rfl

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