Commit 2025-10-26 13:57 84a53aa5
View on Github →chore: rename duplicate lemmas about leadingCoeff (map ..) (#30923) Neither name was great; the new one is more in line with Polynomial.leadingCoeff_map and Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero.