mathlib
e36ae183 - feat(data/set/prod): `set.off_diag` (#16803)

Commit
3 years ago
feat(data/set/prod): `set.off_diag` (#16803) Define the off-diagonal of a set, which is the set of pairs of points whose components are distinct. Co-authored-by: Yaƫl Dillies <yael.dillies@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Author
Parents
Loading