Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 05:12 4e4298e2

View on Github →

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

Estimated changes

Modified archive/100-theorems-list/73_ascending_descending_sequences.lean

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/category_theory/types.lean

modified theorem category_theory.functor_to_types.hcomp

modified theorem category_theory.functor_to_types.map_comp_apply

modified theorem equiv_equiv_iso_hom

modified theorem equiv_equiv_iso_inv

Modified src/computability/tm_computable.lean

modified def turing.evals_to_in_time.refl

modified structure turing.evals_to_in_time

modified def turing.id_computable_in_poly_time

modified structure turing.tm2_computable_in_poly_time

modified def turing.tm2_computable_in_time.to_tm2_computable

modified structure turing.tm2_computable_in_time

modified def turing.tm2_outputs_in_time

Modified src/data/fintype/card.lean

modified theorem fin.sum_univ_succ_above

Modified src/data/list/basic.lean

Modified src/data/list/nodup.lean

Modified src/data/list/pairwise.lean

modified theorem list.pw_filter_map

Modified src/data/list/perm.lean

modified theorem list.perm.inter_append

Modified src/data/list/range.lean

Modified src/data/list/sections.lean

modified theorem list.rel_sections

Modified src/data/list/sigma.lean

modified theorem list.sizeof_erase_dupkeys

modified theorem list.sizeof_kerase

Modified src/data/matrix/basic.lean

modified theorem matrix.col_smul

modified theorem matrix.row_smul

modified theorem matrix.smul_apply

modified theorem matrix.update_column_apply

Modified src/data/mv_polynomial/basic.lean

modified theorem mv_polynomial.support_sum_monomial_coeff

Modified src/data/mv_polynomial/monad.lean

modified theorem mv_polynomial.bind₂_bind₂

modified theorem mv_polynomial.eval₂_hom_bind₁

modified theorem mv_polynomial.eval₂_hom_bind₂

Modified src/geometry/manifold/mfderiv.lean

modified theorem has_mfderiv_within_at.has_mfderiv_at

modified def mfderiv_within

modified theorem unique_mdiff_on.inter

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

modified theorem model_with_corners.to_local_equiv_coe

Modified src/group_theory/archimedean.lean

Modified src/group_theory/coset.lean

Modified src/topology/algebra/continuous_functions.lean

Modified src/topology/algebra/floor_ring.lean

Modified src/topology/algebra/group_completion.lean

modified theorem uniform_space.completion.is_add_group_hom_extension

Modified src/topology/algebra/ordered.lean

modified theorem continuous_within_at_Ico_iff_Iio

modified theorem continuous_within_at_Ioo_iff_Iio

Modified src/topology/algebra/uniform_group.lean

modified theorem to_uniform_space_eq

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/constructions.lean

modified theorem prod_generate_from_generate_from_eq

Modified src/topology/continuous_on.lean

modified theorem continuous_within_at.tendsto

modified theorem continuous_within_at_iff_continuous_at_restrict

Modified src/topology/dense_embedding.lean

modified theorem dense_inducing.tendsto_comap_nhds_nhds

Modified src/topology/metric_space/basic.lean

modified theorem metric.closed_ball_subset_closed_ball

modified theorem metric.diam_union

Modified src/topology/opens.lean

Modified src/topology/order.lean

modified theorem coinduced_le_iff_le_induced

Modified src/topology/path_connected.lean

modified theorem joined.mem_path_component

modified theorem path.truncate_one_one

modified theorem path.truncate_zero_zero