mathlib
d0efe252 - feat(data/finset/prod): diag of union (#13916)

Commit
3 years ago
feat(data/finset/prod): diag of union (#13916) Lemmas about diag and off diag in relation to simple finset constructions.
Author
Parents
Loading