eqOn_set_closure — Mathlib

English

If two ring homomorphisms f,g agree on a set s, then they agree on the subring closure of s.

Русский

Если два гомоморфизма f,g соглашаются на наборе s, то они соглашаются на подкольцо, порождаемое s (замыкание).

LaTeX

$$$ \\operatorname{EqOn}(f,g,s) \\Rightarrow \\operatorname{EqOn}(f,g,\\mathrm{closure}(s)) $$$

Lean4

/-- If two ring homomorphisms are equal on a set, then they are equal on its subring closure. -/
theorem eqOn_set_closure {f g : R →+* S} {s : Set R} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocus g from closure_le.2 h

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