ext_int — Mathlib

English

Two additive equivalences f,g: ℤ ≃+ A are equal if f(1) = g(1).

Русский

Два адиитивных эквивалента ℤ ≃+ A равны, если их значения на 1 совпадают.

LaTeX

$$$$ f,g: \\mathbb{Z} \\simeq_+ A, \\ f(1) = g(1) \\Rightarrow f = g. $$$$

Lean4

/-- Two additive monoid isomorphisms `f`, `g` from `ℤ` to an additive monoid are equal
if `f 1 = g 1`. -/
@[ext high]
theorem ext_int [AddMonoid A] {f g : ℤ ≃+ A} (h1 : f 1 = g 1) : f = g :=
  toAddMonoidHom_injective <| AddMonoidHom.ext_int h1

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