Theorems · Theorem · ring theory

NonUnitalRingHom.eqOn_sclosure

∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {f g : F} {s : Set R},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(NonUnitalSubsemiring.closure s)

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

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringFunLikeNonUnitalNonAssocSemiringNonUnitalRingHomClass