ext_int — Mathlib

English

Two ring homomorphisms f,g: ℤ →+* R are equal if they agree on 1, i.e., if f(1)=g(1).

Русский

Два кольцевых гомоморфизма f,g: ℤ →+* R равны тогда и только тогда, когда они совпадают на 1: f(1)=g(1).

LaTeX

$$$f=g\\;\\Leftrightarrow\\; f(1)=g(1)$$$

Lean4

theorem ext_int {R : Type*} [NonAssocSemiring R] (f g : ℤ →+* R) : f = g :=
  coe_addMonoidHom_injective <| AddMonoidHom.ext_int <| f.map_one.trans g.map_one.symm

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