Def Finset.card

Modification history

2024-05-14 17:58

Mathlib/Data/Finset/Card.lean

chore: deprecate `@[pp_dot]` (#12609) …

Modified Finset.card View on Github →

2024-01-09 08:14

Mathlib/Data/Finset/Card.lean

chore: `pp_dot` on `Finset.card` (#9560)

Modified Finset.card View on Github →

2023-01-16 16:20

Mathlib/Data/Finset/Card.lean

feat: port Data.Finset.Card (#1589)

Added Finset.card View on Github →