mathlib
355645e3 - chore(data/polynomial/*): delete, rename and move lemmas (#12852)

Commit
3 years ago
chore(data/polynomial/*): delete, rename and move lemmas (#12852) - Replace `eval_eq_finset_sum` and `eval_eq_finset_sum'` with `eval_eq_sum_range` and `eval_eq_sum_range'` which are consistent with `evalâ‚‚_eq_sum_range`, `evalâ‚‚_eq_sum_range'` `eval_eq_finset_sum`, `eval_eq_finset_sum'`. Notice that the type of `eval_eq_sum_range'` is different, but this lemma has not been used anywhere in mathlib. - Move the lemma `C_eq_int_cast` from `data/polynomial/degree/definitions.lean` to `data/polynomial/basic.lean`. `C_eq_nat_cast` was already here.
Author
Parents
Loading