Commit 2024-07-01 10:39 e743f360

View on Github →

chore(Polynomial/TrailingDegree): use ENat.toNat, golf (#13652)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

modified theorem Polynomial.natTrailingDegree_le_natTrailingDegree

modified theorem Polynomial.natTrailingDegree_le_of_ne_zero

modified theorem Polynomial.natTrailingDegree_le_trailingDegree

modified theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos

modified theorem Polynomial.trailingDegree_eq_zero

Modified Mathlib/Data/Finset/Lattice.lean

modified theorem Finset.max'_eq_sup'

modified theorem Finset.min'_eq_inf'