Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-08 14:30 cc2e1ece

View on Github →

refactor(*): making mathlib faster again

Estimated changes

modified theorem finset.sum_le_zero'
modified theorem finset.sum_le_zero
modified theorem finset.zero_le_sum'
modified theorem finset.zero_le_sum
modified theorem bit1_zero
modified theorem divp_one
modified theorem divp_self
modified theorem is_conj_refl
modified theorem add_monoid.smul_eq_mul'
modified theorem gpow_neg_one
modified theorem inv_pow
modified theorem list.prod_repeat
modified theorem mul_pow
modified theorem neg_one_gsmul
modified theorem neg_one_pow_eq_or
modified theorem one_div_pow
modified theorem pow_mul
modified theorem is_closed_empty
modified theorem is_closed_univ
modified theorem complex.conj_I
modified theorem complex.conj_neg
modified theorem complex.conj_of_real
modified theorem complex.conj_one
modified theorem complex.conj_zero
modified theorem complex.norm_sq_I
modified theorem complex.norm_sq_one
modified theorem complex.norm_sq_zero
modified theorem complex.of_real_neg
modified theorem finset.coe_image
modified theorem finset.coe_inter
modified theorem finset.coe_union
modified theorem finset.empty_inter
modified theorem finset.empty_union
modified theorem finset.image_id
modified theorem finset.image_to_finset
modified theorem finset.insert_eq
modified theorem finset.inter_assoc
modified theorem finset.inter_comm
modified theorem finset.inter_distrib_left
modified theorem finset.inter_distrib_right
modified theorem finset.inter_empty
modified theorem finset.inter_left_comm
modified theorem finset.inter_right_comm
modified theorem finset.inter_self
modified theorem finset.map_refl
modified theorem finset.max_empty
modified theorem finset.mem_image
modified theorem finset.mem_insert_of_mem
modified theorem finset.mem_insert_self
modified theorem finset.mem_map
modified theorem finset.mem_singleton_self
modified theorem finset.mem_union_left
modified theorem finset.mem_union_right
modified theorem finset.ne_of_mem_erase
modified theorem finset.not_mem_erase
modified theorem finset.not_mem_singleton
modified theorem finset.range_succ
modified theorem finset.sigma_mono
modified theorem finset.union_comm
modified theorem finset.union_distrib_left
modified theorem finset.union_distrib_right
modified theorem finset.union_empty
modified theorem finset.union_idempotent
modified theorem finset.union_right_comm
modified theorem finset.union_self
modified theorem list.concat_cons
modified theorem list.index_of_eq_length
modified theorem list.nil_diff
modified theorem list.prefix_concat
modified theorem list.take_zero
modified theorem polynomial.C_0
modified theorem cardinal.aleph_zero
modified theorem ordinal.lift_type_fin
modified theorem ordinal.one_lt_omega