Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-22 13:47 02ab90cc

View on Github →

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

Estimated changes

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

modified theorem CommRing.colimits.quot_add

modified theorem CommRing.colimits.quot_mul

modified theorem CommRing.colimits.quot_neg

Modified src/algebra/category/Group/limits.lean

Modified src/algebra/group_with_zero/basic.lean

modified theorem is_unit.ne_zero

Modified src/algebra/ordered_group.lean

Modified src/topology/uniform_space/basic.lean

modified theorem filter.has_basis.uniform_continuous_on_iff

modified theorem mem_uniform_prod

modified theorem nhds_basis_uniformity'

modified theorem uniform_continuous_fst

modified theorem uniform_continuous_on_iff_restrict

modified theorem uniform_continuous_snd

modified theorem uniform_space.core_eq

Modified src/topology/uniform_space/completion.lean

modified theorem Cauchy.Cauchy_eq

modified theorem uniform_space.completion.extension_coe

modified theorem uniform_space.completion.extension_unique

Modified test/monotonicity/test_cases.lean