Theorems · Definition · commutative algebra
IsFractionRing
(R : Type u_6) → [inst : CommSemiring R] → (K : Type u_7) → [inst_1 : CommSemiring K] → [Algebra R K] → Prop
IsFractionRing R K states K is the ring of fractions of a commutative ring R.
- Cited by
- 738 results in Mathlib
- Foundations
- Depth 16 from the axioms, rests on 156 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- nonZeroDivisorsproof · cited by 895
- IsLocalizationproof · cited by 636
Cited by859
Results whose statement or proof uses this declaration.
- IsDedekindDomain.HeightOneSpectrum.valuationstatement and proof · cited by 130
- IsDedekindDomain.HeightOneSpectrum.adicCompletionstatement · cited by 93
- IsFractionRing.injectivestatement and proof · cited by 70
- FractionalIdeal.dualstatement and proof · cited by 33
- FractionalIdeal.extendedHomstatement and proof · cited by 26
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletionstatement and proof · cited by 25
- FractionalIdeal.countstatement and proof · cited by 25
- NumberField.FinitePlace.embeddingstatement and proof · cited by 24
- toPrincipalIdealstatement · cited by 23
- IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMapstatement and proof · cited by 23
- ClassGroup.mkstatement and proof · cited by 22
- IsFractionRing.denstatement and proof · cited by 22
Showing the 200 most cited of 859.