ext_mnat — Mathlib

English

Two monoid homomorphisms from Multiplicative Nat to M are equal if they agree on the image of 1 (via ofAdd 1).

Русский

Два гомоморфизма моноида от Multiplicative Nat в M равны, если они совпадают на образе 1 (через ofAdd 1).

LaTeX

$$$f(\\mathrm{ofAdd} \\mathbf{1}) = g(\\mathrm{ofAdd} \\mathbf{1}) \Rightarrow f = g$$$

Lean4

@[ext]
theorem ext_mnat ⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g :=
  MonoidHom.ext fun n ↦ by rw [f.apply_mnat, g.apply_mnat, h]

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