Nat.card versions of Fintype.card lemmas on Sym

Each of the lemmas assuming [Fintype α] and Fintype.card can be restated using Nat.card alone.

instance Sym.instInfiniteOfNeZeroNat (α : Type u_1) {k : ℕ} [Infinite α] [NeZero k] : Infinite (Sym α k)

theorem Sym.natCard_sym_eq_multichoose (α : Type u_1) (k : ℕ) : Nat.card (Sym α k) = (Nat.card α).multichoose k

A version of card_sym_eq_multichoose that does not need finiteness.

theorem Sym.natCard_sym_eq_choose (α : Type u_1) (k : ℕ) : Nat.card (Sym α k) = (Nat.card α + k - 1).choose k

A version of card_sym_eq_choose that does not need finiteness.

instance Sym2.instInfinite (α : Type u_1) [Infinite α] : Infinite (Sym2 α)

instance Sym2.instInfiniteSubtypeIsDiag (α : Type u_1) [Infinite α] : Infinite { a : Sym2 α // a.IsDiag }

instance Sym2.instInfiniteSubtypeNotIsDiag (α : Type u_1) [Infinite α] : Infinite { a : Sym2 α // ¬a.IsDiag }

theorem Sym2.natCard_subtype_diag (α : Type u_1) : Nat.card { a : Sym2 α // a.IsDiag } = Nat.card α

theorem Sym2.natCard_subtype_not_diag (α : Type u_1) : Nat.card { a : Sym2 α // ¬a.IsDiag } = (Nat.card α).choose 2

theorem Sym2.ncard_diagSet (α : Type u_1) : diagSet.ncard = Nat.card α

theorem Sym2.ncard_diagSet_compl (α : Type u_1) : diagSetᶜ.ncard = (Nat.card α).choose 2

theorem Sym2.natCard (α : Type u_1) : Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Type stars and bars for the case n = 2.