Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-01 09:10 c5e0d103

View on Github →

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

Estimated changes

Modified archive/100-theorems-list/82_cubing_a_cube.lean

Modified docs/tutorial/category_theory/intro.lean

Modified src/algebra/algebra/subalgebra.lean

modified theorem algebra.bijective_algebra_map_iff

Modified src/algebra/continued_fractions/computation/approximations.lean

Modified src/algebra/continued_fractions/computation/correctness_terminating.lean

Modified src/algebra/continued_fractions/computation/translations.lean

Modified src/algebra/divisibility.lean

Modified src/algebra/group/prod.lean

modified theorem mul_equiv.coe_prod_comm

Modified src/algebra/quandle.lean

modified inductive rack.pre_envel_group_rel'

Modified src/algebra/ring_quot.lean

modified theorem ring_quot.lift_alg_hom_mk_alg_hom_apply

modified theorem ring_quot.rel.neg

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/category_theory/hom_functor.lean

Modified src/category_theory/isomorphism.lean

Modified src/category_theory/limits/creates.lean

modified def category_theory.lift_colimit

Modified src/category_theory/limits/limits.lean

modified theorem category_theory.limits.colimit.ι_map

modified theorem category_theory.limits.colimit.ι_post

modified theorem category_theory.limits.colimit.ι_pre

modified theorem category_theory.limits.has_colimit.iso_of_nat_iso_hom_desc

modified theorem category_theory.limits.has_colimit.of_cocones_iso

modified theorem category_theory.limits.has_limit.of_cones_iso

modified def category_theory.limits.is_colimit.cocone_point_unique_up_to_iso

modified theorem category_theory.limits.limit.pre_π

Modified src/category_theory/limits/shapes/binary_products.lean

modified theorem category_theory.limits.coprod.associator_naturality

modified def category_theory.limits.coprod.desc

modified theorem category_theory.limits.coprod.desc_comp

modified theorem category_theory.limits.coprod.map_codiag

modified theorem category_theory.limits.coprod.map_inl_inr_codiag

modified theorem category_theory.limits.coprod.map_swap

modified theorem category_theory.limits.prod.diag_map_fst_snd

modified theorem category_theory.limits.prod.lift_fst_comp_snd_comp

modified theorem category_theory.limits.prod.lift_map

modified theorem category_theory.limits.prod.map_swap

Modified src/category_theory/limits/shapes/biproducts.lean

modified def category_theory.limits.biproduct.is_colimit

modified theorem category_theory.limits.has_binary_biproduct.mk

Modified src/category_theory/limits/shapes/finite_limits.lean

modified theorem category_theory.limits.has_finite_wide_pullbacks_of_has_finite_limits

modified theorem category_theory.limits.has_finite_wide_pushouts_of_has_finite_limits

Modified src/category_theory/limits/shapes/images.lean

modified def category_theory.limits.image.iso_strong_epi_mono

modified theorem category_theory.limits.image.iso_strong_epi_mono_hom_comp_ι

modified theorem category_theory.limits.image.iso_strong_epi_mono_inv_comp_mono

Modified src/category_theory/limits/shapes/kernel_pair.lean

modified def category_theory.is_kernel_pair.cancel_right

modified def category_theory.is_kernel_pair.cancel_right_of_mono

Modified src/category_theory/limits/shapes/regular_mono.lean

modified def category_theory.regular_of_is_pullback_fst_of_regular

modified def category_theory.regular_of_is_pullback_snd_of_regular

Modified src/category_theory/monad/algebra.lean

Modified src/category_theory/monoidal/of_chosen_finite_products.lean

Modified src/category_theory/skeletal.lean

Modified src/data/lazy_list/basic.lean

modified theorem lazy_list.append_assoc

modified theorem lazy_list.mem_cons

modified def lazy_list.pmap

Modified src/data/matrix/notation.lean

modified theorem matrix.mul_vec_cons

Modified src/data/multiset/fold.lean

modified theorem multiset.fold_add

modified theorem multiset.fold_eq_foldl

modified theorem multiset.fold_eq_foldr

modified theorem multiset.fold_erase_dup_idem

Modified src/data/mv_polynomial/equiv.lean

modified def mv_polynomial.ring_equiv_congr

Modified src/order/filter/bases.lean

modified theorem filter.generate_eq_generate_inter

modified structure filter.has_countable_basis

Modified src/order/filter/basic.lean

Modified src/ring_theory/ideal/operations.lean

Modified src/tactic/linarith/datatypes.lean

Modified src/topology/algebra/multilinear.lean

added def continuous_multilinear_map.apply_add_hom

Modified src/topology/category/Top/adjunctions.lean

Modified src/topology/list.lean

Modified src/topology/local_extr.lean

modified theorem is_local_extr_on.comp_continuous_on

modified theorem is_local_extr_on.is_local_extr

modified theorem is_local_max_on.comp_continuous_on

modified theorem is_local_min_on.comp_continuous_on

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/lipschitz.lean

Modified test/finish2.lean

Modified test/finish4.lean