Theorem IsFractionRing.isInvariant

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) …

Modified IsFractionRing.isInvariant View on Github →

2026-05-08 14:51

Mathlib/RingTheory/Invariant/Basic.lean

feat(RingTheory/Localization, FieldTheory/Galois): refactor fraction field action API and add fixingSubgroup lemmas (#38377) …

Added IsFractionRing.isInvariant View on Github →