Theorem DirectLimit.star_def

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