Theorem DirectLimit.Ring.lift_of

Modification history

2026-04-28 09:23
Mathlib/Algebra/Colimit/DirectLimit.lean
refactor: make `DirectLimit.lift` the simp-normal form of the bundled versions (#38593) …
Modified DirectLimit.Ring.lift_ofView on Github →
2024-12-21 08:53
Mathlib/Algebra/Colimit/DirectLimit.lean
feat: algebraic hierarchy on DirectLimit (#19893) …
Added DirectLimit.Ring.lift_ofView on Github →