Theorem DirectLimit.NonUnitalStarRing.hom_ext

Modification history

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