Theorem Sym2.cardinalMk_prod_eq_two_mul_cardinalMk_fromRel

Modification history

2026-10-01 17:54
Mathlib/Data/Sym/Sym2/Card.lean
feat(Data/Sym/Sym2/Card): cardinality theorems about `Sym2 α` (#36442)
Added Sym2.cardinalMk_prod_eq_two_mul_cardinalMk_fromRelView on Github →