Commit 2026-04-23 23:45 1c558eb4

View on Github →

feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit (#38308) add Star, InvolutiveStar, StarMul, StarAddMonoid, StarRing, and StarModule instances to DirectLimit, following the pattern of existing algebraic structures in Mathlib.Algebra.Colimit.DirectLimit. also add the universal property API (of, lift, hom_ext, of_f, lift_of) for StarRing.

Estimated changes

Modified Mathlib/Algebra/Colimit/DirectLimit.lean

added theorem DirectLimit.NonUnitalRing.hom_ext

added theorem DirectLimit.NonUnitalRing.lift_of

added theorem DirectLimit.NonUnitalRing.of_f

added theorem DirectLimit.NonUnitalStarRing.hom_ext

added theorem DirectLimit.NonUnitalStarRing.lift_of

added theorem DirectLimit.NonUnitalStarRing.of_f

added theorem DirectLimit.star_def