Theorems · Inductive type · ring theory
NonUnitalSubringClass
(S : Type u_1) → (R : Type u) → [NonUnitalNonAssocRing R] → [SetLike S R] → Prop
NonUnitalSubringClass S R states that S is a type of subsets s ⊆ R that
are both a multiplicative submonoid and an additive subgroup.
- Defined in
- Mathlib.RingTheory.NonUnitalSubring.Defs
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- NonUnitalNonAssocRingSetLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLikestatement · cited by 1,084
- NonUnitalNonAssocRingstatement · cited by 354
Cited by20
Results whose statement or proof uses this declaration.
- NonUnitalSubringClass.subtypestatement and proof · cited by 6
- NonUnitalSubring.unitizationstatement and proof · cited by 2
- AlgHomClass.unitization_injectivestatement and proof · cited by 2
- NonUnitalStarSubalgebra.unitizationStarAlgEquivstatement and proof · cited by 1
- AlgHomClass.unitization_injective'statement and proof · cited by 1
- NonUnitalSubalgebra.unitizationAlgEquivstatement and proof · cited by 1
- NonUnitalSubring.ofClassstatement and proof · cited by 1
- NonUnitalSubring.unitization_applystatement and proof · cited by 0
- NonUnitalSubring.unitization_rangestatement and proof · cited by 0
- NonUnitalStarSubalgebra.unitization_injectivestatement and proof · cited by 0
- NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coestatement and proof · cited by 0
- cfcₙ_memstatement and proof · cited by 0