ext — Mathlib

English

Let f and g be multiplicative homomorphisms from M to N. If f and g agree on every element of M, then f and g are equal.

Русский

Пусть 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 [Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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