[Merged by Bors] - feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit #38308

Closed

drocta wants to merge 24 commits intoleanprover-community:masterfrom

drocta:star-direct-limit

Commits on Apr 17, 2026

add Star and InvolutiveStar instances for DirectLimit
drocta
committed

Commits on Apr 20, 2026

Merge branch 'master' into star-direct-limit
drocta
authored

Commits on Apr 21, 2026

add DirectLimit.NonUnitalRing.lift and use it to shorten Ring.lift and StarRing.lift
drocta
committed
Merge branch 'star-direct-limit' of https://github.com/drocta/mathlib4 into star-direct-limit
drocta
committed
Merge branch 'master' into star-direct-limit
drocta
authored
make instance of Star for DirectLimit more concise
drocta
committed
Merge branch 'star-direct-limit' of https://github.com/drocta/mathlib4 into star-direct-limit
drocta
committed
use the existing proofs for star_add and star_mul in the instance of StarRing for DirectLimit instead of repeating them
drocta
committed
add NonUnitalRing.of and use it to shorten Ring.of and StarRing.of
drocta
committed
tidy syntax for Ring.lift and StarRing.lift
drocta
committed
Merge branch 'master' into star-direct-limit
drocta
authored
improve whitespace
drocta
committed
add of_f, lift_of, hom_ext for DirectLimit.NonUnitalRing
drocta
committed

Commits on Apr 22, 2026

Commits on Apr 23, 2026