Commit 2023-08-12 22:08 a28c6c6c

View on Github →

feat: weaken assumptions on Polynomial.map lemmas (#6544) The assumptions on these lemmas seem to be too strong - R does not need to be a field, only a division ring, and S does not need to be a division ring, only a nontrivial semiring.

Estimated changes

modified theorem Polynomial.degree_map
modified theorem Polynomial.leadingCoeff_map
modified theorem Polynomial.monic_map_iff
modified theorem Polynomial.natDegree_map