Theorem Algebra.isInvariant_of_isGalois

Modification history

2025-01-20 15:19
Mathlib/RingTheory/Invariant.lean
feat(RingTheory/Invariant): Galois extensions satisfy `Algebra.IsInvariant` (#20106) …
Added Algebra.isInvariant_of_isGaloisView on Github →