basic): add `mk_sum` (#15261)

Commit

3 years ago

feat(ring_theory/localization/basic): add `mk_sum` (#15261) add a missing lemma stating that $\frac{\sum_i, a\_i}{b}=\sum_i\frac{a_i}b$

Author

jjaassoonn

Parents