mathlib3
7833dbe4 - lint(algebra/*): fix some lint errors (#13058)

Commit

3 years ago

lint(algebra/*): fix some lint errors (#13058) * add some docstrings to additive versions; * make `with_zero.ordered_add_comm_monoid` reducible.

Author

urkud

Parents