Theorem IntermediateField.finrank_le_of_le_right

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_le_of_le_rightView on Github →