Theorem Algebra.isInvariant_of_isGalois

Modification history

2026-06-23 10:39

Mathlib/RingTheory/Invariant/Basic.lean

chore(RingTheory/Invariant/Basic): split file by imports (#40928) …

Modified Algebra.isInvariant_of_isGalois View on Github →

2025-01-20 15:19

Mathlib/RingTheory/Invariant.lean

feat(RingTheory/Invariant): Galois extensions satisfy `Algebra.IsInvariant` (#20106) …

Added Algebra.isInvariant_of_isGalois View on Github →