α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]