Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 01:44 3e381ad0

View on Github →

chore(ring_theory/*): split lines (#6316)

Estimated changes

Modified src/ring_theory/algebra_tower.lean

Modified src/ring_theory/dedekind_domain.lean

Modified src/ring_theory/derivation.lean

Modified src/ring_theory/free_comm_ring.lean

modified theorem free_comm_ring.exists_finite_support

modified theorem free_comm_ring.restriction_of

Modified src/ring_theory/ideal/basic.lean

Modified src/ring_theory/ideal/operations.lean

modified theorem ideal.mem_radical_of_pow_mem

modified theorem ideal.span_singleton_mul_span_singleton

modified theorem ring_hom.lift_of_surjective_comp

Modified src/ring_theory/integral_closure.lean

Modified src/ring_theory/integral_domain.lean

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/jacobson_ideal.lean

modified theorem ideal.is_local.le_jacobson

modified theorem ideal.is_primary_of_is_maximal_radical

Modified src/ring_theory/localization.lean