Theorems · Definition · commutative algebra
IsIntegrallyClosed
(R : Type u_1) → [CommRing R] → Prop
R is integrally closed if all integral elements of Frac(R) are also elements of R.
This definition uses FractionRing R to denote Frac(R). See isIntegrallyClosed_iff
if you want to choose another field of fractions for R.
- Cited by
- 203 results in Mathlib
- Foundations
- Depth 45 from the axioms, rests on 491 definitions · uses propext, Quot.sound
- Assumes
- CommRing
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.
- CommRingstatement and proof · cited by 17,173
- FractionRingproof · cited by 200
- IsIntegrallyClosedInproof · cited by 23
Cited by218
Results whose statement or proof uses this declaration.
- FractionalIdeal.dualstatement and proof · cited by 33
- Algebra.intNormstatement and proof · cited by 28
- Ideal.relNormstatement and proof · cited by 23
- Ideal.spanNormstatement and proof · cited by 19
- IsIntegrallyClosed.isIntegral_iffstatement and proof · cited by 13
- Algebra.adjoin.powerBasis'statement and proof · cited by 11
- minpoly.isIntegrallyClosed_eq_field_fractions'statement and proof · cited by 11
- isIntegrallyClosed_iffstatement · cited by 10
- minpoly.isIntegrallyClosed_dvdstatement and proof · cited by 9
- Algebra.intTracestatement and proof · cited by 9
- coeIdeal_differentIdealstatement and proof · cited by 8
- KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMkstatement and proof · cited by 8
Showing the 200 most cited of 218.