Theorem IsGaloisGroup.card_eq_finrank'

Modification history

2026-08-18 10:50
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
chore(FieldTheory/Galois/IsGaloisGroup): remove FaithfulSMul assumptions (#41208) …
Modified IsGaloisGroup.card_eq_finrank'View on Github →
2026-06-20 15:40
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
refactor(FieldTheory/Galois/IsGaloisGroup): generalize `mulEquivAlgEquiv` to domains (#40822) …
Modified IsGaloisGroup.card_eq_finrank'View on Github →
2026-06-08 10:43
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
feat(RingTheory/RamificationInertia/Basic): ramification-inertia formula for finite flat extensions (#39189) …
Added IsGaloisGroup.card_eq_finrank'View on Github →