Theorem IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'

Modification history

2025-02-03 08:48
Mathlib/FieldTheory/PurelyInseparable.lean
refactor(FieldTheory): split `Mathlib.FieldTheory.Purelyinseparable` (#21343)
Modified IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'View on Github →
2025-01-30 19:40
Mathlib/FieldTheory/PurelyInseparable.lean
feat(FieldTheory): `F⟮a⟯ = F⟮a ^ q ^ n⟯` in `ExpChar q` for separable `a` (#21249) …
Added IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'View on Github →