mathlib
9556784a - chore(ring_theory/*): Fix lint (#16350)

Commit

3 years ago

chore(ring_theory/*): Fix lint (#16350) Satisfy the `fintype_finite` and `check_reducibility` linters.

Author

YaelDillies

Parents