Commit 2025-04-07 10:22 41dda67e

View on Github →

feat(FieldTheory/Normal): A quadratic extension is normal (#23452)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.splits_of_degree_eq_two

added theorem Polynomial.splits_of_natDegree_eq_two

Modified Mathlib/FieldTheory/Normal/Basic.lean

added theorem normal_of_finrank_eq_two