Theorem IsFractionRing.isInvariant_of_isIntegral

Modification history

2026-05-28 13:10
Mathlib/RingTheory/Invariant/Basic.lean
feat(FieldTheory/Galois/IsGaloisGroup): add version of `IsGaloisGroup.to_isFractionRing` assuming only `IsIntegral` (#39091) …
Added IsFractionRing.isInvariant_of_isIntegralView on Github →