Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-23 15:29 61ed14e2

View on Github →

lint(*): split long lines (#6833)

Estimated changes

Modified src/analysis/convex/caratheodory.lean

Modified src/analysis/specific_limits.lean

Modified src/data/padics/hensel.lean

Modified src/data/set/basic.lean

Modified src/geometry/euclidean/basic.lean

modified theorem euclidean_geometry.dist_reflection

Modified src/geometry/manifold/algebra/monoid.lean

Modified src/geometry/manifold/basic_smooth_bundle.lean

modified theorem basic_smooth_bundle_core.mem_chart_source_iff

Modified src/geometry/manifold/charted_space.lean

Modified src/geometry/manifold/instances/real.lean

Modified src/geometry/manifold/times_cont_mdiff.lean

modified theorem smooth.mdifferentiable_within_at

modified theorem times_cont_mdiff_within_at.of_succ

Modified src/logic/function/basic.lean

modified theorem function.update_noteq

modified def set.piecewise

Modified src/order/galois_connection.lean

modified def galois_coinsertion.monotone_intro

Modified src/order/zorn.lean

Modified src/topology/instances/real.lean

modified theorem real.mem_closure_iff

Modified src/topology/local_homeomorph.lean

modified def local_homeomorph.prod

modified theorem local_homeomorph.prod_to_local_equiv

Modified src/topology/sheaves/presheaf.lean

modified theorem Top.presheaf.pushforward.comp_hom_app

modified theorem Top.presheaf.pushforward.comp_inv_app

modified def Top.presheaf.pushforward_map

Modified src/topology/tactic.lean

Modified src/topology/uniform_space/separation.lean

modified theorem uniform_space.separation_quotient.lift_mk

Modified src/topology/uniform_space/uniform_convergence.lean

Modified src/topology/uniform_space/uniform_embedding.lean