Theorem DirectLimit.NonUnitalStarRing.of_f

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.of_fView 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.of_fView on Github →