Theorems · Theorem · commutative algebra

RingHom.eqOn_sclosure

∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f g : R →+* S} {s : Set R},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subsemiring.closure s)

If two ring homomorphisms are equal on a set, then they are equal on its subsemiring closure.

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring