Theorem IntermediateField.finrank_dvd_of_le_left

Modification history

2025-06-23 08:19
Mathlib/FieldTheory/IntermediateField/Algebraic.lean
feat(FieldTheory/IntermediateField/Algebraic): Containment of intermediate fields implies divisibility of `finrank` (#26191) …
Added IntermediateField.finrank_dvd_of_le_leftView on Github →