Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-27 15:26 3550f4f3

View on Github →

feat(*): remaining preliminaries for Haar measure (#3541) Define has_mul (finset α) more convenient formulation of is_compact.finite_compact_cover some lemma additions

Estimated changes

added theorem finset.coe_mul
added theorem finset.mem_mul
added theorem finset.mul_card_le
added theorem finset.mul_def
added theorem finset.mul_mem_mul
added theorem set.inv_subset
added theorem set.inv_subset_inv
modified theorem set.preimage_mul_right_one'
added theorem set.preimage_congr
modified theorem measurable.mul
modified theorem measurable_mul
added theorem measurable_mul_left
added theorem measurable_mul_right