Theorems · Inductive type · commutative algebra
Subring
(R : Type u) → [NonAssocRing R] → Type u
Subring R is the type of subrings of R. A subring of R is a subset s that is a
multiplicative submonoid and an additive subgroup. Note in particular that it shares the
same 0 and 1 as R.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Cited by
- 602 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonAssocRingstatement · cited by 483
Cited by743
Results whose statement or proof uses this declaration.
- RingHom.rangestatement · cited by 138
- Subring.closurestatement and proof · cited by 78
- Subring.toSubsemiringstatement and proof · cited by 71
- Valuation.integerstatement · cited by 68
- Valuation.valuationSubringproof · cited by 56
- Subring.mapstatement and proof · cited by 33
- Subring.opstatement and proof · cited by 32
- ValuationSubring.toSubringstatement · cited by 32
- Subalgebra.toSubringstatement · cited by 30
- Subfield.mapproof · cited by 30
- Subfield.comapproof · cited by 29
- Subring.centerstatement · cited by 28
Showing the 200 most cited of 743.