Zulip Chat Archive
Stream: triage
Topic: PR !4#26489: refactor(RingTheory/RingHom): factor out pro...
Random Issue Bot (Jul 20 2025 at 14:08):
Today I chose PR #26489 for discussion!
refactor(RingTheory/RingHom): factor out proofs for Algebra.FinitePresentation
Created by @Christian Merten (@chrisflav) on 2025-06-28
Labels: t-algebra
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Sep 15 2025 at 14:13):
Today I chose PR #26489 for discussion!
refactor(RingTheory/RingHom): factor out proofs for Algebra.FinitePresentation
Created by @Christian Merten (@chrisflav) on 2025-06-28
Labels: t-algebra
Is this PR still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Sep 16 2025 at 05:23):
Reviewed
Last updated: Dec 20 2025 at 21:32 UTC