Theorem Polynomial.Separable.map_irreducible_of_isPurelyInseparable

Modification history

2025-02-03 08:48

Mathlib/FieldTheory/PurelyInseparable.lean

refactor(FieldTheory): split `Mathlib.FieldTheory.Purelyinseparable` (#21343)

Modified Polynomial.Separable.map_irreducible_of_isPurelyInseparable View on Github →

2024-03-01 09:34

Mathlib/FieldTheory/PurelyInseparable.lean

feat(FieldTheory/PurelyInseparable): some more results for purely inseparable extension (#10882) …

Added Polynomial.Separable.map_irreducible_of_isPurelyInseparable View on Github →