coe_ringHom_commutes — Mathlib

English

The two routes from an algebra equivalence to a RingHom coincide, i.e., coercions commute up to equality.

Русский

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

LaTeX

$$$ (e.toAlgHom) = (e : A_1 \to_{R} A_2)^{\text{RingHom}} $$$

Lean4

/-- The two paths coercion can take to a `RingHom` are equivalent -/
theorem coe_ringHom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) :=
  rfl

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