[Merged by Bors] - chore: remove superseded small_of_fintype

[TwoFX]

---

[YaelDillies]

This already exists as small_of_fintype (but you can replace the Fintype assumption by Finite and rename it to the correct name of Finite.toSmall)

[TwoFX]

This already exists as small_of_fintype (but you can replace the Fintype assumption by Finite and rename it to the correct name of Finite.toSmall)

Thanks, I unified the two versions. Why do you say that Finite.toSmall is the correct name instead of Finite.small? I'm not aware of any rule that mandates adding the to.

[YaelDillies]

Forgetful inheritance instances should be named A.toB. The rule is extended to Prop-valued typeclasses where it's not quite "inheritance" anymore.

[TwoFX]

@YaelDillies this sounds strange to me, doesn't toSmall break the rule that Prop-valued theorems should use snake case?

[YaelDillies]

It's not a theorem, it's an instance. That's where the difference is. See eg GCDMonoid.toIsIntegrallyClosed.

[TwoFX]

Okay, I've renamed it to Finite.toSmall.

[YaelDillies]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[fpvandoorn]

Renamed the PR to reflect the changes from the review

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style