ext — Mathlib

English

Let f and g be monoid homomorphisms from M to N. If f and g agree on every element of M, then f = g.

Русский

Пусть f и g — гомоморфизмы моноида M → N. Если для каждого элемента x ∈ M выполняется f(x) = g(x), то f = g.

LaTeX

$$$\\big( \\forall x \\in M,\; f\\,x = g\\,x \\big) \\Rightarrow f = g$$$

Lean4

@[to_additive (attr := ext)]
theorem ext [MulOne M] [MulOne N] ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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