mathlib3
499a4a89 - feat(group_theory/index): `fintype_of_index_ne_zero` (#13225)

Commit

3 years ago

feat(group_theory/index): `fintype_of_index_ne_zero` (#13225) This PR adds `fintype_of_index_ne_zero`.

Author

tb65536

Parents