Commit 2023-08-02 18:06 63f711cb

View on Github →

chore(Data/Polynomial/FieldDivision): use by_cases instead of if (#6314) This is easier to remove from the classical locale in future, and is arguably more readable

Estimated changes

Modified Mathlib/Data/Polynomial/FieldDivision.lean

modified theorem Polynomial.degree_div_le

modified theorem Polynomial.map_dvd_map'

modified theorem Polynomial.map_mod

modified theorem Polynomial.not_irreducible_C

modified theorem Polynomial.prime_of_degree_eq_one