mathlib

709c73b2 - feat(category_theory/Fintype): some lemmas and `Fintype_to_Profinite`. (#7491)

feat(category_theory/Fintype): some lemmas and `Fintype_to_Profinite`. (#7491) Adding some lemmas for morphisms on `Fintype` as functions, as well as `Fintype_to_Profinite`. Part of the LTE. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>