Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-26 23:04 6e2980ce

View on Github →

chore(*): reflow some long lines (#4794)

Estimated changes

Modified archive/sensitivity.lean

Modified src/algebra/algebra/basic.lean

modified def alg_equiv.of_alg_hom

Modified src/algebra/algebra/operations.lean

Modified src/algebra/archimedean.lean

Modified src/algebra/associated.lean

modified theorem irreducible_of_prime

modified theorem prime_of_associated

Modified src/algebra/big_operators/basic.lean

modified theorem ring_hom.map_prod

Modified src/algebra/big_operators/intervals.lean

Modified src/algebra/big_operators/ring.lean

modified theorem finset.prod_powerset_insert

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/category/CommRing/adjunctions.lean

Modified src/algebra/char_p.lean

modified theorem char_p_of_prime_pow_injective

Modified src/algebra/continued_fractions/computation/basic.lean

Modified src/algebra/direct_limit.lean

modified theorem add_comm_group.direct_limit.lift_add

modified theorem add_comm_group.direct_limit.lift_sub

modified theorem add_comm_group.direct_limit.of_add

modified theorem add_comm_group.direct_limit.of_sub

modified theorem module.direct_limit.of.zero_exact_aux

modified theorem ring.direct_limit.induction_on

modified theorem ring.direct_limit.of.zero_exact_aux

modified theorem ring.direct_limit.of_pow

Modified src/algebra/gcd_monoid.lean

Modified src/algebra/geom_sum.lean

modified theorem op_geom_series

Modified src/algebra/monoid_algebra.lean