Theorem IntermediateField.normal_iff_normalClosure_eq

Modification history

2023-09-07 00:04
Mathlib/FieldTheory/NormalClosure.lean
refactor(FieldTheory/NormalClosure): change definition and add API (#6163) …
Added IntermediateField.normal_iff_normalClosure_eqView on Github →