chore: pp_dot on Finset.card (#9560)

leanprover-community · Jan 9, 2024 · aa782a7 · aa782a7
1 parent 2b75532
commit aa782a7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
@@ -40,7 +40,7 @@ namespace Finset
 variable {s t : Finset α} {a b : α}
 
 /-- `s.card` is the number of elements of `s`, aka its cardinality. -/
-def card (s : Finset α) : ℕ :=
+@[pp_dot] def card (s : Finset α) : ℕ :=
   Multiset.card s.1
 #align finset.card Finset.card