Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-16 09:19 bc7a201e

View on Github →

feat(*): Pointwise monoids have distributive negations (#14114) More instances of has_distrib_neg:

function.injective.has_distrib_neg, function.surjective.has_distrib_neg
add_opposite, mul_opposite
set, finset, filter

Estimated changes

Modified src/algebra/ring/basic.lean

Modified src/algebra/star/unitary.lean

Modified src/data/finset/n_ary.lean

added theorem finset.image₂_distrib_subset_left

added theorem finset.image₂_distrib_subset_right

Modified src/data/finset/pointwise.lean

added theorem finset.add_mul_subset

added theorem finset.mul_add_subset

Modified src/data/set/basic.lean

added theorem set.image2_distrib_subset_left

added theorem set.image2_distrib_subset_right

Modified src/data/set/pointwise.lean

added theorem set.add_mul_subset

added theorem set.mul_add_subset

Modified src/linear_algebra/general_linear_group.lean

modified theorem matrix.GL_pos.coe_neg

added theorem matrix.GL_pos.coe_neg_GL

Modified src/linear_algebra/special_linear_group.lean

modified theorem matrix.special_linear_group.coe_int_neg

modified theorem matrix.special_linear_group.coe_neg

Modified src/order/filter/n_ary.lean

added theorem filter.map₂_distrib_le_left

added theorem filter.map₂_distrib_le_right

Modified src/order/filter/pointwise.lean

added theorem filter.add_mul_subset

added theorem filter.mul_add_subset