pointwise): `s ∩ t * s ∪ t ⊆ s * t` (#17961)

Commit

2 years ago

feat(data/finset/pointwise): `s ∩ t * s ∪ t ⊆ s * t` (#17961) and distributivity of `set.to_finset`/`set.finite.to_finset` over algebraic operations.

Author

YaelDillies

Parents