Zulip Chat Archive
Stream: triage
Topic: PR #6476: feat(algebra/ring/boolean_ring): boolean_algebr...
Random Issue Bot (Oct 24 2021 at 14:18):
Today I chose PR 6476 for discussion!
feat(algebra/ring/boolean_ring): boolean_algebra.to_boolean_ring
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-02-28
Labels: help wanted, WIP, awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Bryan Gin-ge Chen (Oct 24 2021 at 15:11):
The plan is still to make PR(s) creating ext lemmas for ring per https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236476.20boolean_algebra.2Eto_boolean_ring
Random Issue Bot (Dec 08 2021 at 14:20):
Today I chose PR 6476 for discussion!
feat(algebra/ring/boolean_ring): boolean_algebra.to_boolean_ring
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-02-28
Labels: help wanted, WIP, awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 20 2022 at 14:13):
Today I chose PR 6476 for discussion!
feat(algebra/ring/boolean_ring): boolean_algebra.to_boolean_ring
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-02-28
Labels: help wanted, WIP, awaiting-author
Is this PR still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Mar 20 2022 at 14:20):
Am on it. We will soon be able to turn this into a categorical fact.
Last updated: Dec 20 2023 at 11:08 UTC