Theorem isAlgebraic_of_isFractionRing

Modification history

2026-06-15 13:16

Mathlib/RingTheory/Localization/Integral.lean

feat(RingTheory/Invariant/Basic): generalize `Ideal.Quotient.normal` to `IsFractionRing` (#40247) …

Modified isAlgebraic_of_isFractionRing View on Github →

2024-01-09 09:24

Mathlib/RingTheory/Localization/Integral.lean

feat: Define `intNorm` and `intTrace`. (#9265)

Added isAlgebraic_of_isFractionRing View on Github →