Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-02 00:43 eb616cf4

View on Github →

chore(*): split long lines (#2913)

Estimated changes

modified theorem fin_enum.finset.mem_enum
modified theorem fin_enum.mem_pi
modified theorem fin_enum.pi.mem_enum
modified def fin_enum.pi
modified theorem finset.coe_inter
modified theorem finset.coe_union
modified theorem finset.exists_max_image
modified theorem finset.exists_min_image
modified theorem finset.fold_insert
modified theorem finset.image_to_finset
modified theorem finset.insert_union_distrib
modified theorem finset.mem_insert_of_mem
modified theorem finset.mem_union_left
modified theorem finset.mem_union_right
modified def finset.pi.cons
modified theorem finset.pi.cons_ne
modified theorem finset.pi.cons_same
modified theorem finset.sdiff_subset_sdiff
modified theorem finset.sigma_eq_bind
modified theorem int.cast_eq_zero
modified theorem int.cast_inj
modified theorem int.coe_nat_bit0
modified theorem int.coe_nat_bit1
modified theorem int.coe_nat_inj'
modified theorem int.coe_nat_le
modified theorem int.coe_nat_lt
modified theorem int.shiftr_neg_succ
modified theorem int.test_bit_ldiff
modified theorem list.exists_of_mem_map
modified theorem list.map_subset_iff
modified def list.split_on_p_aux
modified theorem list.func.pointwise_nil
modified theorem list.nodup_erase_eq_filter
modified theorem list.nodup_join
modified theorem list.nth_le_index_of
modified theorem list.map_sub_range'
modified theorem pequiv.single_trans_single
modified theorem pnat.bit0_le_bit0
modified theorem pnat.bit0_le_bit1
modified theorem pnat.bit1_le_bit0
modified theorem pnat.bit1_le_bit1
modified theorem polynomial.coeff_add
modified theorem polynomial.coeff_derivative
modified theorem polynomial.coeff_sub
modified theorem polynomial.derivative_eval
modified theorem quotient.lift_beta
modified theorem quotient.lift_on_beta
modified theorem cau_seq.const_inv
modified theorem computation.destruct_map
modified theorem wseq.destruct_flatten
modified theorem wseq.nth_terminates_le
modified theorem plift.rec.constant
modified theorem ulift.rec.constant
modified theorem relation.equivalence_join
modified theorem coe_bit1