mathlib
aba57d4d - feat(combinatorics/double_counting): Special cases (#17647)

Commit

3 years ago

feat(combinatorics/double_counting): Special cases (#17647) GIve special cases of `card_mul_le_card_mul` and `card_mul_le_card_mul'` when `m = n = 1`.

Author

YaelDillies

Parents

f2c46488

mathlib aba57d4d - feat(combinatorics/double_counting): Special cases (#17647)

mathlib
aba57d4d - feat(combinatorics/double_counting): Special cases (#17647)