coe_ringHom_inj_iff — Mathlib

English

Two ring equivalences f and g are equal iff their underlying ring homs are equal.

Русский

Две кольцевые эквивалентности равны тогда и только тогда, когда их базовые кольцевые гомоморфизмы равны.

LaTeX

$$$$ f = g \\;\\iff\\; (f : R \\to+* S) = g. $$$$

Lean4

theorem coe_ringHom_inj_iff {R S : Type*} [NonAssocSemiring R] [NonAssocSemiring S] (f g : R ≃+* S) :
    f = g ↔ (f : R →+* S) = g :=
  ⟨fun h => by rw [h], fun h => ext <| RingHom.ext_iff.mp h⟩

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