Theorems · Inductive type · ring theory
Ring
Type u → Type u
A Ring is a Semiring with negation making it an additive group.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 7,463 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by9,053
Results whose statement or proof uses this declaration.
- ModuleCatstatement · cited by 1,429
- ModuleCat.carrierstatement and proof · cited by 997
- AffineSubspacestatement · cited by 871
- Valuationstatement · cited by 823
- AffineMapstatement · cited by 674
- Ideal.Quotient.mkstatement and proof · cited by 610
- ModuleCat.ofstatement and proof · cited by 594
- spectrumstatement and proof · cited by 510
- Affine.Simplexstatement · cited by 471
- minpolystatement and proof · cited by 439
- IsIntegralstatement and proof · cited by 427
- affineSpanstatement and proof · cited by 417
Showing the 200 most cited of 9,053.