Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 08:39 159542ad

View on Github →

chore(*): split some long lines (#5742)

Estimated changes

modified theorem min_pow_dvd_add
modified theorem pow_eq_zero
modified def invertible.map
modified theorem invertible_unique
modified theorem has_deriv_within_at.union
modified theorem has_fderiv_within_at.union
modified theorem nnnorm_sum_le
modified theorem tsum_of_norm_bounded
modified theorem deriv_within_arctan
modified def uliftable.down_map
modified def uliftable.up_map
modified theorem filter.realizer.of_equiv_σ
modified theorem filter.realizer.tendsto_iff
modified theorem equiv.refl_to_local_equiv
modified theorem local_equiv.of_set_symm
modified theorem local_equiv.restr_target
modified theorem local_equiv.trans_target
modified def fintype.of_surjective
modified theorem mem_of_mem_perms_of_list
modified theorem mem_perms_of_list_iff
modified theorem set.to_finset_inj
modified theorem typevec.const_append1
modified def typevec.of_subtype
modified def typevec.rel_last'
modified theorem typevec.repeat_eq_append1
modified theorem typevec.repeat_eq_iff_eq
modified theorem typevec.subtype_val_nil
modified def typevec.to_subtype
modified def slim_check.sum.shrink
modified theorem isometry.comp
modified theorem is_compact.tendsto_subseq'
modified theorem eq_of_uniformity_inf_nhds
modified theorem separation_rel_comap