Theorems · Inductive type · ring theory

NonUnitalSubsemiringClass

(S : Type u_1) → (R : outParam (Type u)) → [NonUnitalNonAssocSemiring R] → [SetLike S R] → Prop

NonUnitalSubsemiringClass S R states that S is a type of subsets s ⊆ R that are both an additive submonoid and also a multiplicative subsemigroup.

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Cited by

22 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringSetLike