Commit 2026-06-02 14:25 b0fad949

View on Github →

feat: Nat.card lemmas for Sym and Sym2 (#38741) These are just translations of the Fintype counterparts.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Sym/Card.lean

modified theorem Sym2.card_subtype_diag

Created Mathlib/Data/Sym/NatCard.lean

added theorem Sym.natCard_sym_eq_choose

added theorem Sym.natCard_sym_eq_multichoose

added theorem Sym2.natCard_subtype_diag

added theorem Sym2.natCard_subtype_not_diag

added theorem Sym2.ncard_diagSet

added theorem Sym2.ncard_diagSet_compl

Modified Mathlib/Data/Sym/Sym2.lean

added def Sym2.diagElem

added def Sym2.diagElemEquiv

added theorem Sym2.diagElem_mk

added theorem Sym2.diag_diagElem