Commit 2023-05-24 12:14 100392f8

View on Github →

feat: port Algebra.DirectLimit (#4052) A few times rw [RingHom.map_neg] worked, rw [(FreeCommRing.lift _).map_neg] failed, and rw [(FreeCommRing.lift <explicit function>).map_neg] succeeded. So there was some "sweet spot" where rw would fail, and if you either gave it strictly less or strictly more information it would succeed. Other than that, not much to say.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectLimit.lean

added def AddCommGroup.DirectLimit.lift

added theorem AddCommGroup.DirectLimit.lift_of

added theorem AddCommGroup.DirectLimit.lift_unique

added theorem AddCommGroup.DirectLimit.of.zero_exact

added def AddCommGroup.DirectLimit.of

added theorem AddCommGroup.DirectLimit.of_f

added def AddCommGroup.DirectLimit

added theorem DirectedSystem.map_map

added theorem DirectedSystem.map_self

added theorem Field.DirectLimit.exists_inv

added theorem Module.DirectLimit.exists_of

added def Module.DirectLimit.lift

added theorem Module.DirectLimit.lift_of

added theorem Module.DirectLimit.lift_unique

added theorem Module.DirectLimit.of.zero_exact

added theorem Module.DirectLimit.of.zero_exact_aux

added def Module.DirectLimit.of

added theorem Module.DirectLimit.of_f

added theorem Module.DirectLimit.toModule_totalize_of_le

added theorem Module.DirectLimit.totalize_of_le

added theorem Module.DirectLimit.totalize_of_not_le

added def Module.DirectLimit

added theorem Ring.DirectLimit.exists_of

added theorem Ring.DirectLimit.induction_on

added def Ring.DirectLimit.lift

added theorem Ring.DirectLimit.lift_of

added theorem Ring.DirectLimit.lift_unique

added theorem Ring.DirectLimit.of.zero_exact

added theorem Ring.DirectLimit.of.zero_exact_aux2

added theorem Ring.DirectLimit.of.zero_exact_aux

added theorem Ring.DirectLimit.of_f

added theorem Ring.DirectLimit.of_injective

added def Ring.DirectLimit

Modified Mathlib/RingTheory/FreeCommRing.lean

added theorem FreeCommRing.of_cons