eq_of_eqOn_topM — Mathlib

English

If two monoid homomorphisms f and g agree on all of M (i.e., on the top submonoid), then f = g.

Русский

Если два гомоморфизма f и g согласны на всём множестве M (на верхнем подмоноде), то f = g.

LaTeX

$$$\forall f,g : M \to* N,\ (\forall x \in M, f(x)=g(x)) \Rightarrow f=g$$$

Lean4

@[to_additive]
theorem eq_of_eqOn_topM {f g : M →* N} (h : Set.EqOn f g (⊤ : Submonoid M)) : f = g :=
  ext fun _ => h trivial

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