mathlib
2a155208
- chore(data/polynomial): generalize `aeval_eq_sum_range` to `comm_semiring` (#8037)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(data/polynomial): generalize `aeval_eq_sum_range` to `comm_semiring` (#8037) This pair of lemmas did not need any `comm_ring` assumptions, so I put them in a new section with weaker typeclass assumptions.
Author
Vierkantor
Parents
3937c1b2
Loading