eq_of_eqOn_set_top — Mathlib

English

Let f,g: R →ₙ+* S be two nonunital ring homomorphisms. If they agree on the whole domain, then f = g.

Русский

Пусть f,g: R →ₙ+* S — два гомоморфизма колец без единицы. Если они совпадают на всём R, то они равны.

LaTeX

$$$\mathrm{EqOn}(f,g,\top_{R}) \Rightarrow f=g$$$

Lean4

theorem eq_of_eqOn_set_top {f g : R →ₙ+* S} (h : Set.EqOn f g (⊤ : NonUnitalSubring R)) : f = g :=
  ext fun _x => h trivial

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