Theorem Normal.isIntegral

Modification history

2024-05-16 14:20

Mathlib/FieldTheory/Normal.lean

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

Modified Normal.isIntegral View on Github →

2023-06-09 06:37

Mathlib/FieldTheory/Normal.lean

feat: port FieldTheory.Normal (#4856)

Added Normal.isIntegral View on Github →