Theorem IntermediateField.essFiniteType_iff

Modification history

2026-01-20 18:20

Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

feat(RingTheory): field extension over perfect fields are smooth (#32617)

Added IntermediateField.essFiniteType_iff View on Github →