coe_nonUnitalRingHom_inj_iff — Mathlib

English

Two ring equivalences are equal iff their underlying non-unital ring homs are equal.

Русский

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

LaTeX

$$$$ f = g \\iff (f : R \\to\\n+' S) = g. $$$$

Lean4

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

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