mathlib3
d5861954 - feat(data/finset/pointwise): Missing operations (#12865)

Commit
3 years ago
feat(data/finset/pointwise): Missing operations (#12865) Define `-s`, `s⁻¹`, `s - t`, `s / t`, `s +ᵥ t`, `s • t`, `s -ᵥ t`, `a • s`, `a +ᵥ s` for `s`, `t` finsets, `a` scalar. Provide a bare API following what is already there for `s + t`, `s * t`.
Author
Parents
Loading