Theorems · Theorem · ring theory

NonUnitalRingHom.eq_of_eqOn_sdense

∀ {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] {s : Set R},
  NonUnitalSubsemiring.closure s = ⊤ → ∀ {f g : F}, Set.EqOn (⇑f) (⇑g) s → f = g

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringFunLikeNonUnitalNonAssocSemiringNonUnitalRingHomClass