Theorem Fintype.card_piFinset_const

Modification history

2024-07-31 05:14
Mathlib/Data/Fintype/BigOperators.lean
feat: Lemmas specialised to `piFinset fun _ : Fin n ↦ s` (#15329) …
Added Fintype.card_piFinset_constView on Github →