Commit 2021-11-25 12:14 7d8a1e07

View on Github →

feat(data/polynomial/eval): random eval lemmas (#10470) note that the geom_sum import only adds the geom_sum file itself; all other files were imported already

Estimated changes

Modified src/algebra/geom_sum.lean

added theorem one_geom_sum

modified theorem op_geom_sum

modified theorem op_geom_sum₂

Modified src/data/polynomial/eval.lean

added theorem polynomial.eval_dvd

added theorem polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero

added theorem polynomial.eval_geom_sum