Commit 2023-03-27 18:03 7664848d

View on Github →

feat: s ∩ t * s ∪ t ⊆ s * t (#1619) Match https://github.com/leanprover-community/mathlib/pull/17961

Estimated changes

Modified Mathlib/Data/Finset/NAry.lean

added theorem Finset.image₂_inter_union_subset

added theorem Finset.image₂_union_inter_subset

added theorem Set.Finite.toFinset_image2

added theorem Set.toFinset_image2

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.card_one

added theorem Finset.card_smul_finset

added theorem Finset.image_smul_comm

added theorem Finset.image_smul_distrib

added theorem Finset.inter_mul_union_subset

added theorem Finset.union_mul_inter_subset

added theorem Set.Finite.toFinset_mul

added theorem Set.Finite.toFinset_one

added theorem Set.Finite.toFinset_smul

added theorem Set.Finite.toFinset_smul_set

added theorem Set.Finite.toFinset_vsub

added theorem Set.toFinset_mul

added theorem Set.toFinset_one

added theorem Set.toFinset_smul

added theorem Set.toFinset_smul_set

added theorem Set.toFinset_vsub

Modified Mathlib/Data/Polynomial/RingDivision.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.image2_inter_union_subset

added theorem Set.image2_union_inter_subset

Modified Mathlib/Data/Set/Pointwise/Basic.lean

added theorem Set.inter_mul_union_subset

added theorem Set.union_mul_inter_subset

Modified Mathlib/Data/Set/Pointwise/Finite.lean

added theorem Set.finite_one

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.image_smul_comm

added theorem Set.image_smul_distrib