eq_of_eqOn_stop — Mathlib

English

If closure s = ⊤, then equality of ring homomorphisms on s implies equality on all R.

Русский

Если замыкание s даёт ⊤, то совпадение отображений на s означает совпадение на всём R.

LaTeX

$$$\\text{closure}(s)=\\top \\Rightarrow (f=g\\text{ on } s) \\Rightarrow f=g$$$

Lean4

theorem eq_of_eqOn_stop {f g : R →+* S} (h : Set.EqOn f g (⊤ : Subsemiring R)) : f = g :=
  ext fun _ => h (mem_top _)

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