Commit 2024-11-28 14:24 cbd40933

View on Github →

feat: {a, b} * s = a • s ∪ b • s (#19406) and other simple pointwise lemmas. From GrowthInGroups (LeanCamCombi)

Estimated changes

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

added theorem Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul

added theorem Set.mem_invOf_smul_set

added theorem Set.mem_smul_set_inv

added theorem Set.mul_pair

modified theorem Set.op_smul_set_subset_mul

added theorem Set.pair_mul

added theorem Set.smul_set_subset_mul