mathlib
2cf5d19e - chore(algebra/*): Fix lint (#16128)

Commit
3 years ago
chore(algebra/*): Fix lint (#16128) Satisfy the `fintype_finite` and `to_additive_doc` linters.
Author
Parents
Loading