Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 11:03 e6896117

View on Github →

chore({data/{finset,set},order/filter}/pointwise): Reorganize files (#14021) Order the three files more similarly. The idea is to order things as:

  • Arithmetic notation typeclasses, and lemmas that don't depend on algebraic structure for them:
    • 0 and 1
    • - and ⁻¹
    • + and *
    • - and /
  • monoid-like instances, interleaved with the corresponding lemmas (some of them are used for the instances themselves, and more will be in the future)
  • •
  • -ᵥ
  • scalar instances

Estimated changes

modified theorem finset.coe_pow
modified theorem finset.image_mul_right'
modified theorem finset.image_mul_right
modified theorem set.Inter_inv
modified theorem set.Union_inv
modified theorem set.compl_inv
modified theorem set.empty_pow
modified def set.fintype_mul
modified theorem set.image_mul_left'
modified theorem set.image_mul_left
modified theorem set.image_mul_right'
modified theorem set.image_mul_right
modified theorem set.inter_inv
modified theorem set.inv_preimage
modified theorem set.mem_inv
modified theorem set.mul_univ
modified theorem set.pow_mem_pow
modified theorem set.pow_subset_pow
modified theorem set.preimage_mul_left_one'
modified theorem set.preimage_mul_left_one
modified theorem set.preimage_mul_right_one'
modified theorem set.preimage_mul_right_one
deleted def set.singleton_hom
modified theorem set.subset_mul_left
modified theorem set.subset_mul_right
modified theorem set.union_inv
modified theorem set.univ_mul
modified theorem set.univ_mul_univ
modified theorem filter.comap_mul_comap_le
modified theorem filter.map_inv'
added theorem filter.pow_mem_pow
modified theorem filter.tendsto.div_div
modified theorem filter.tendsto.inv_inv