Commit 2025-09-29 11:36 b62f2279
View on Github →feat(Algebra/Polynomial/Degree/Support): add missing as_sum_range_C_mul_X_pow' (#30046)
This PR adds the missing lemma as_sum_range_C_mul_X_pow' which is analogous to as_sum_range'. I also changed the argument n to be implicit in as_sum_range', because it can be inferred.