mathlib3
a22cd4d7 - chore(algebra/group_with_zero): nolint (#3254)

Commit

5 years ago

chore(algebra/group_with_zero): nolint (#3254) Adding two doc strings to make the file lint-free again. cf. #3253.

Author

bryangingechen

Parents