Theorem DirectLimit.NonUnitalStarRing.lift_comp_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) …
Added DirectLimit.NonUnitalStarRing.lift_comp_ofView on Github →