mathlib3
48fd9f25 - chore(data/list/big_operators): rename vars, reorder lemmas (#11433)

Commit
4 years ago
chore(data/list/big_operators): rename vars, reorder lemmas (#11433) * use better variable names; * move lemmas to proper sections; * relax `[comm_semiring R]` to `[semiring R]` in `dvd_sum`.
Author
Parents
Loading