Commit 2026-04-28 09:23 aae58b3b

View on Github →

refactor: make DirectLimit.lift the simp-normal form of the bundled versions (#38593) A bunch of lift_of lemmas about the bundled version are now somewhat redundant. For now I do not deprecate these, as the lemma that they would be deprecated in favor of currently has the wrong name. I'll make a separate PR that renames all the mis-named lemmas first.

Estimated changes

Modified Mathlib/Algebra/Colimit/DirectLimit.lean

added theorem DirectLimit.Module.lift_comp_of

added theorem DirectLimit.NonUnitalRing.lift_comp_of

modified theorem DirectLimit.NonUnitalRing.lift_of

modified theorem DirectLimit.NonUnitalRing.of_f

added theorem DirectLimit.NonUnitalStarRing.lift_comp_of

modified theorem DirectLimit.NonUnitalStarRing.lift_of

modified theorem DirectLimit.NonUnitalStarRing.of_f

added theorem DirectLimit.Ring.lift_comp_of

modified theorem DirectLimit.Ring.lift_of

modified theorem DirectLimit.Ring.of_f

Modified Mathlib/Algebra/Colimit/Module.lean

Modified Mathlib/Algebra/Colimit/Ring.lean

Modified Mathlib/Order/DirectedInverseSystem.lean

added theorem DirectLimit.mk_apply