Theorem Set.ncard_insert_eq_ite

Modification history

2024-04-14 10:41

Mathlib/Data/Set/Card.lean

chore: remove autoImplicit from more files (#11798) …

Modified Set.ncard_insert_eq_ite View on Github →

2023-06-06 18:52

Mathlib/Data/Set/Ncard.lean

feat: port Data.Set.Ncard (#4591) …

Added Set.ncard_insert_eq_ite View on Github →