Theorem IntermediateField.finrank_fixedField_eq_card

Modification history

2025-07-30 17:21

Mathlib/FieldTheory/Galois/Basic.lean

refactor(FieldTheory/Galois): Switch from `Fintype` to `Finite` (#25997) …

Modified IntermediateField.finrank_fixedField_eq_card View on Github →

2023-06-16 05:40

Mathlib/FieldTheory/Galois.lean

feat: port FieldTheory.Galois (#5115)

Added IntermediateField.finrank_fixedField_eq_card View on Github →