Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-28 04:55 dc34b216

View on Github →

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

Estimated changes

Modified src/control/functor/multivariate.lean

Modified src/control/monad/writer.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/data/nat/basic.lean

Modified src/data/nat/gcd.lean

Modified src/data/nat/modeq.lean

Modified src/data/nat/multiplicity.lean

Modified src/data/nat/totient.lean

Modified src/geometry/euclidean/circumcenter.lean

modified theorem affine.simplex.sum_centroid_weights_with_circumcenter

Modified src/geometry/manifold/charted_space.lean

modified def structomorph.trans

Modified src/geometry/manifold/local_invariant_properties.lean

modified theorem structure_groupoid.local_invariant_prop.lift_prop_on_mono

Modified src/meta/coinductive_predicates.lean

Modified src/meta/expr.lean

Modified src/order/bounded_lattice.lean

Modified src/order/filter/extr.lean

modified theorem is_extr_filter.comp_tendsto

Modified src/order/filter/lift.lean

Modified src/set_theory/cardinal.lean

modified theorem cardinal.lift_lift

Modified src/tactic/chain.lean

Modified src/tactic/converter/binders.lean

Modified src/tactic/equiv_rw.lean

Modified src/tactic/find_unused.lean

Modified src/tactic/finish.lean

Modified src/tactic/group.lean

modified theorem tactic.group.gpow_trick_sub

Modified src/tactic/linarith/frontend.lean

Modified src/tactic/linarith/lemmas.lean

modified theorem linarith.int.coe_nat_bit0_mul

modified theorem linarith.int.coe_nat_bit1_mul

modified theorem linarith.int.coe_nat_mul_bit0

modified theorem linarith.int.coe_nat_mul_bit1

modified theorem linarith.mul_zero_eq

modified theorem linarith.nat_eq_subst

modified theorem linarith.nat_le_subst

modified theorem linarith.nat_lt_subst

modified theorem linarith.zero_mul_eq

Modified src/tactic/norm_cast.lean

Modified src/tactic/nth_rewrite/default.lean

Modified src/tactic/omega/find_ees.lean

Modified src/tactic/omega/nat/dnf.lean

Modified src/tactic/omega/nat/main.lean

Modified src/tactic/push_neg.lean

Modified src/tactic/ring.lean

modified theorem tactic.ring.pow_add_rev_right

Modified src/tactic/ring2.lean

Modified src/tactic/ring_exp.lean

Modified src/tactic/simp_result.lean

Modified src/tactic/simp_rw.lean

Modified src/topology/sheaves/presheaf_of_functions.lean

Modified src/topology/sheaves/sheaf_of_functions.lean

Modified test/group.lean

Modified test/lint.lean

Modified test/random.lean

Modified test/where.lean