eqOn_set_closure — Mathlib

English

If two nonunital ring homomorphisms f,g: R →ₙ+* S agree on a subset s ⊆ R, then they agree on the NonUnitalSubring closure of s.

Русский

Если два гомоморфизма колец без единицы f,g: R →ₙ+* S совпадают на подмножестве s ⊆ R, то они совпадают на замыкании подпольного подкольца, порождаемого s.

LaTeX

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

Lean4

/-- If two ring homomorphisms are equal on a set, then they are equal on its
`NonUnitalSubring` 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

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