eq_of_eqOn_dense — Mathlib

English

If closure(s) = ⊤ and two multiplicative homomorphisms agree on s, then the homomorphisms are equal.

Русский

Если closure(s) = ⊤ и два умножение-гомоморфизма совпадают на s, то они равны.

LaTeX

$$$\\mathrm{closure}(s) = \\top \\Rightarrow f = g \\text{ if } f|_{s} = g|_{s}$$$

Lean4

@[to_additive]
theorem eq_of_eqOn_dense {s : Set M} (hs : closure s = ⊤) {f g : M →ₙ* N} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_top <| hs ▸ eqOn_closure h

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