Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 07:39 ca679aca

View on Github →

chore(algebra/direct_limit): linting (#4411)

Estimated changes

Modified src/algebra/direct_limit.lean

deleted theorem add_comm_group.direct_limit.directed_system

modified theorem add_comm_group.direct_limit.lift_unique

modified theorem add_comm_group.direct_limit.of.zero_exact

modified def add_comm_group.direct_limit

modified theorem module.direct_limit.exists_of

modified theorem module.direct_limit.lift_unique

modified theorem module.direct_limit.of.zero_exact_aux

modified theorem ring.direct_limit.exists_of

modified theorem ring.direct_limit.induction_on

modified theorem ring.direct_limit.lift_unique

modified theorem ring.direct_limit.of.zero_exact_aux

modified theorem ring.direct_limit.of_injective

modified theorem ring.direct_limit.polynomial.exists_of