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-02-13 06:13

Mathlib/RingTheory/Invariant.lean

feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions (#20899) …

Added Algebra.isInvariant_of_isGalois'View on Github →