Commit 2024-11-05 13:37 e9946a76
View on Github →refactor: make Set.fintypeMul/Set.fintypeDiv instances (#18073)
Looks like Set.fintypeMul was not made an instance in https://github.com/leanprover-community/mathlib3/pull/3240 out of fear that they would make the Mul (Set α) instance globally accessible.
From LeanCamCombi