Theorems · Theorem · ring theory

NonUnitalRingHom.eqOn_set_closure

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

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

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRing