Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-01 19:15 684f4f50

View on Github →

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

Estimated changes

Modified src/algebra/group_power/lemmas.lean

modified theorem nat.cast_le_pow_sub_div_sub

modified theorem semiconj_by.cast_nat_mul_right

Modified src/algebra/group_with_zero/power.lean

modified theorem commute.fpow_fpow_self

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/analysis/convex/extrema.lean

Modified src/category_theory/adjunction/limits.lean

modified def category_theory.adjunction.functoriality_counit'

modified def category_theory.adjunction.functoriality_counit

modified def category_theory.adjunction.functoriality_unit'

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

Modified src/data/nat/cast.lean

modified theorem nat.cast_dvd

Modified src/data/qpf/multivariate/constructions/cofix.lean

modified theorem mvqpf.cofix.ext_mk

Modified src/deprecated/group.lean

Modified src/deprecated/ring.lean

Modified src/deprecated/subgroup.lean

modified theorem is_add_subgroup.gsmul_mem

modified theorem is_subgroup.coe_gpow

Modified src/field_theory/algebraic_closure.lean

modified theorem is_alg_closed.degree_eq_one_of_irreducible

Modified src/linear_algebra/finite_dimensional.lean

modified theorem findim_eq_zero

modified theorem finite_dimensional.span_of_finite

Modified src/linear_algebra/lagrange.lean

Modified src/linear_algebra/linear_independent.lean

Modified src/number_theory/pell.lean

modified theorem pell.eq_of_xn_modeq

modified theorem pell.eq_of_xn_modeq_le

Modified src/order/omega_complete_partial_order.lean

modified theorem omega_complete_partial_order.continuous_hom.comp_assoc

Modified src/tactic/interval_cases.lean

Modified src/tactic/local_cache.lean

Modified src/tactic/squeeze.lean