Theorem IsPurelyInseparable.isIntegral'

Modification history

2025-02-03 08:48

Mathlib/FieldTheory/PurelyInseparable.lean

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

Modified IsPurelyInseparable.isIntegral'View on Github →

2024-05-16 14:20

Mathlib/FieldTheory/PurelyInseparable.lean

refactor: Turn Algebra.IsAlgebraic and Algebra.IsIntegral into classes (#12761) …

Added IsPurelyInseparable.isIntegral'View on Github →