Theorem IntermediateField.normalClosure_def''

Modification history

2025-10-16 07:33
Mathlib/FieldTheory/Normal/Closure.lean
feat: notation for galois group (#30266) …
Modified IntermediateField.normalClosure_def''View on Github →
2023-09-07 00:04
Mathlib/FieldTheory/NormalClosure.lean
refactor(FieldTheory/NormalClosure): change definition and add API (#6163) …
Added IntermediateField.normalClosure_def''View on Github →