Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-14 11:12 ae193735

View on Github →

feat(data/set/pointwise/smul): a • (s \ t) = a • s \ a • t (#17927) Scalar multiplication distributes over set and symmetric difference.

Estimated changes

modified theorem set.smul_set_inter
modified theorem set.smul_set_inter₀
added theorem set.smul_set_sdiff
added theorem set.smul_set_sdiff₀
added theorem set.smul_set_symm_diff
modified theorem set.smul_set_univ
modified theorem set.smul_univ
added theorem set.smul_univ₀'
modified theorem set.smul_univ₀