Commit 2023-07-28 16:09 5c3c589c

View on Github →

feat(RingTheory/Polynomial/ScaleRoots): reduce typeclass assumptions (#6213)

Estimated changes

Modified Mathlib/Logic/Nontrivial.lean

added theorem Subsingleton.eq_one

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

modified theorem Polynomial.scaleRoots_aeval_eq_zero

modified theorem Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero

modified theorem Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero