mathlib3
ae193735 - feat(data/set/pointwise/smul): `a • (s \ t) = a • s \ a • t` (#17927)

Commit
3 years ago
feat(data/set/pointwise/smul): `a • (s \ t) = a • s \ a • t` (#17927) Scalar multiplication distributes over set and symmetric difference.
Author
Parents
Loading