Theorems · Definition · ring theory
NonUnitalSubring.toSubsemigroup
{R : Type u} → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R → Subsemigroup RThe underlying submonoid of a NonUnitalSubring.
- Defined in
- Mathlib.RingTheory.NonUnitalSubring.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- NonUnitalNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonUnitalNonAssocRingstatement and proof · cited by 354
- Subsemigroupstatement and proof · cited by 323
- AddSubmonoid.toAddSubsemigroupproof · cited by 198
- AddSubsemigroup.carrierproof · cited by 198
- NonUnitalSubringstatement and proof · cited by 185
- NonUnitalSubsemiring.toAddSubmonoidproof · cited by 56
- NonUnitalSubring.toNonUnitalSubsemiringproof · cited by 15
- NonUnitalSubsemiring.toSubsemigroupproof · cited by 12
Cited by13
Results whose statement or proof uses this declaration.
- NonUnitalSubring.mapproof · cited by 19
- NonUnitalSubring.comapproof · cited by 15
- NonUnitalSubring.prodproof · cited by 9
- NonUnitalSubring.topologicalClosureproof · cited by 4
- NonUnitalSubring.mem_iSup_of_directedproof · cited by 2
- NonUnitalSubring.mk'_toSubsemigroupstatement and proof · cited by 1
- NonUnitalSubring.toSubsemigroup_strictMonostatement · cited by 1
- NonUnitalSubring.nonUnitalCommRingTopologicalClosureproof · cited by 0
- NonUnitalSubring.toSubsemigroup_injectivestatement and proof · cited by 0
- NonUnitalSubring.toSubsemigroup_monostatement · cited by 0
- NonUnitalSubring.coe_toSubsemigroupstatement · cited by 0
- NonUnitalSubring.sInf_toSubsemigroupstatement · cited by 0