Zulip Chat Archive
Stream: triage
Topic: issue #18164: Tracking: attribute semireducible/irreducible
Random Issue Bot (Mar 08 2023 at 14:09):
Today I chose issue 18164 for discussion!
Tracking: attribute semireducible/irreducible
Created by @Johan Commelin (@jcommelin) on 2023-01-13
Labels: needs-refactor, mathport
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Mar 08 2023 at 14:11):
Yes, see today's other thread: https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/PR.20.2318179.3A.20feat.28linear_algebra.2Fclifford.29.3A.20make.20clifford_a.2E.2E.2E
Random Issue Bot (Jul 19 2023 at 14:07):
Today I chose issue 18164 for discussion!
Tracking: attribute semireducible/irreducible
Created by @Johan Commelin (@jcommelin) on 2023-01-13
Labels: needs-refactor, mathport
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC