Theorem DirectLimit.NonUnitalStarRing.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.NonUnitalStarRing.lift_of View on Github →

2026-04-23 23:45

Mathlib/Algebra/Colimit/DirectLimit.lean

feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit (#38308) …

Added DirectLimit.NonUnitalStarRing.lift_of View on Github →