Theorems · Definition · commutative algebra
Subring.toSubsemiring
{R : Type u} → [inst : NonAssocRing R] → Subring R → Subsemiring RReinterpret a Subring as a Subsemiring.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Subringstatement and proof · cited by 602
- NonAssocRingstatement and proof · cited by 483
- Subsemiringstatement · cited by 456
Cited by104
Results whose statement or proof uses this declaration.
- IntermediateField.adjoinproof · cited by 382
- Subring.mapproof · cited by 33
- Subring.opproof · cited by 32
- Subring.unopproof · cited by 25
- spinGroupproof · cited by 23
- Subring.comapproof · cited by 22
- Subring.subtypeproof · cited by 22
- Subfield.subtypeproof · cited by 16
- Subring.prodproof · cited by 11
- Subring.toAddSubgroupproof · cited by 11
- Set.integerproof · cited by 8
- Subring.copyproof · cited by 7