Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-29 13:12 16776539

View on Github →

chore(*): long lines (#6939) Except for URLs, references to books, and src/tactic/*, this should be very close to the last of our long lines.

Estimated changes

Modified src/data/pnat/xgcd.lean

Modified src/data/polynomial/iterated_deriv.lean

Modified src/data/sym2.lean

Modified src/meta/expr_lens.lean

Modified src/meta/rb_map.lean

Modified src/order/complete_lattice.lean

Modified src/order/conditionally_complete_lattice.lean

Modified src/order/fixed_points.lean

Modified src/order/lexicographic.lean

Modified src/order/ord_continuous.lean

Modified src/order/pilex.lean

Modified src/order/preorder_hom.lean

Modified src/set_theory/game/nim.lean

Modified src/set_theory/ordinal_arithmetic.lean

Modified src/set_theory/schroeder_bernstein.lean

Modified src/set_theory/surreal.lean

Modified src/system/random/basic.lean

modified def rand.random_series_r

Modified src/tactic/abel.lean

Modified src/tactic/cache.lean

Modified src/tactic/chain.lean

Modified src/tactic/equiv_rw.lean

Modified src/tactic/fin_cases.lean

Modified src/tactic/hint.lean

Modified src/topology/algebra/uniform_ring.lean

modified theorem uniform_space.ring_sep_quot

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/omega_complete_partial_order.lean

Modified src/topology/sheaves/forget.lean

Modified src/topology/sheaves/sheaf.lean

Modified src/topology/sheaves/sheaf_condition/equalizer_products.lean

Modified src/topology/sheaves/stalks.lean

Modified src/topology/subset_properties.lean

Modified src/topology/uniform_space/absolute_value.lean

Modified src/topology/uniform_space/compact_separated.lean