mathlib3
98c62bd0 - feat(data/set/prod): add theorems about `λ x, (x, x)` (#15604)

Commit
3 years ago
feat(data/set/prod): add theorems about `λ x, (x, x)` (#15604) From the sphere eversion project. Also swap LHS with RHS in `set.diagonal_eq_range` and rename it to `set.range_diag`. Co-authored-by: Oliver Nash <oliver.nash@gmail.com>
Author
Parents
Loading