eqOn_field_closure — Mathlib

English

If two ring homomorphisms agree on a set s, they agree on the closure of s.

Русский

Если два кольцеобразных гомоморфизма совпадают на множестве s, они совпадают на замыкании s.

LaTeX

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

Lean4

/-- If two ring homomorphisms are equal on a set, then they are equal on its subfield closure. -/
theorem eqOn_field_closure {f g : K →+* L} {s : Set K} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocusField g from closure_le.2 h

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