Theorem List.exists_pw_disjoint_with_card

Modification history

2025-02-25 14:06
Mathlib/Data/Fintype/EquivFin.lean
chore(Data/Set/Finite): avoid importing algebra in `Data.Set.Finite` (#21870) …
Modified List.exists_pw_disjoint_with_cardView on Github →
2025-02-20 09:21
Mathlib/Data/Fintype/Card.lean
chore(Data/Fintype): split `Fintype/Card.lean` (#21840) …
Modified List.exists_pw_disjoint_with_cardView on Github →
2023-10-26 16:24
Mathlib/Data/Fintype/Card.lean
feat (GroupTheory.Perm.Cycle.PossibleTypes) : cycleTypes of perm (#7433) …
Added List.exists_pw_disjoint_with_cardView on Github →