From 298e0e0dda8ccdfe6eeca0b8acf8615d45c4c296 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Oct 2024 11:05:21 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20`card=20(=CE=B9=20=E2=86=92=E2=82=80=20?=
 =?UTF-8?q?=CE=B1)=20=3D=20card=20=CE=B1=20^=20card=20=CE=B9`=20(#17807)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

From PFR
---
 Mathlib/Data/Finsupp/Fintype.lean | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Finsupp/Fintype.lean b/Mathlib/Data/Finsupp/Fintype.lean
index 0f5b2e08e49867..b347815decf835 100644
--- a/Mathlib/Data/Finsupp/Fintype.lean
+++ b/Mathlib/Data/Finsupp/Fintype.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Alex J. Best
 -/
 import Mathlib.Data.Finsupp.Defs
-import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Fintype.BigOperators
 
 /-!
 
@@ -14,17 +14,19 @@ Some lemmas on the combination of `Finsupp`, `Fintype` and `Infinite`.
 
 -/
 
+variable {ι α : Type*} [DecidableEq ι] [Fintype ι] [Zero α] [Fintype α]
 
-noncomputable instance Finsupp.fintype {ι π : Sort _} [DecidableEq ι] [Zero π] [Fintype ι]
-    [Fintype π] : Fintype (ι →₀ π) :=
+noncomputable instance Finsupp.fintype : Fintype (ι →₀ α) :=
   Fintype.ofEquiv _ Finsupp.equivFunOnFinite.symm
 
-instance Finsupp.infinite_of_left {ι π : Sort _} [Nontrivial π] [Zero π] [Infinite ι] :
-    Infinite (ι →₀ π) :=
-  let ⟨_, hm⟩ := exists_ne (0 : π)
+instance Finsupp.infinite_of_left [Nontrivial α] [Infinite ι] : Infinite (ι →₀ α) :=
+  let ⟨_, hm⟩ := exists_ne (0 : α)
   Infinite.of_injective _ <| Finsupp.single_left_injective hm
 
-instance Finsupp.infinite_of_right {ι π : Sort _} [Infinite π] [Zero π] [Nonempty ι] :
-    Infinite (ι →₀ π) :=
+instance Finsupp.infinite_of_right [Infinite α] [Nonempty ι] : Infinite (ι →₀ α) :=
   Infinite.of_injective (fun i => Finsupp.single (Classical.arbitrary ι) i)
     (Finsupp.single_injective (Classical.arbitrary ι))
+
+variable (ι α) in
+@[simp] lemma Fintype.card_finsupp : card (ι →₀ α) = card α ^ card ι := by
+  simp [card_congr Finsupp.equivFunOnFinite]