Theorems · Definition · commutative algebra
Subring.toNonUnitalSubring
{R : Type u} → [inst : NonAssocRing R] → Subring R → NonUnitalSubring RTurn a Subring into a NonUnitalSubring by forgetting that it contains 1.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- NonAssocRing
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.
- Subringstatement and proof · cited by 602
- NonAssocRingstatement and proof · cited by 483
- NonUnitalSubringstatement · cited by 185
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
- Subsemiring.toSubmonoidproof · cited by 153
- Subring.toSubsemiringproof · cited by 71
- Subring.neg_mem'proof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- ValuationSubring.nonunits_lestatement · cited by 1
- Subring.one_mem_toNonUnitalSubringstatement · cited by 0
- Subring.centralizer_toNonUnitalSubringstatement · cited by 0
- NonUnitalSubring.toSubring_toNonUnitalSubringstatement and proof · cited by 0
- Subring.toNonUnitalSubring_toSubringstatement and proof · cited by 0