Commit 2026-04-28 12:20 d104ce73

View on Github →

chore(Algebra/Polynomial/Splits): [CommRing R] [IsSimpleRing R] -> [Field R] (#38591)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

modified theorem Polynomial.Splits.adjoin_rootSet_eq_range

modified theorem Polynomial.Splits.aeval_eq_prod_aroots

modified theorem Polynomial.Splits.image_rootSet

modified theorem Polynomial.Splits.mem_range_of_isRoot

modified theorem Polynomial.Splits.of_splits_map

modified theorem Polynomial.Splits.roots_map