Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-19 09:56 c9fc9bf7

View on Github →

refactor(order/filter/pointwise): Cleanup (#12789)

  • Reduce typeclass assumptions from monoid to has_mul
  • Turn lemmas into instances
  • Use hom classes rather than concrete hom types
  • Golf

Estimated changes

modified theorem set.image_mul
modified theorem filter.comap_mul_comap_le
modified def filter.map_monoid_hom
modified theorem filter.mem_mul
modified theorem filter.mem_one
modified theorem filter.mul_mem_mul
modified theorem filter.ne_bot.mul
added theorem filter.one_mem_one
modified theorem filter.tendsto.mul_mul