Zulip Chat Archive
Stream: triage
Topic: PR #1822: [WIP] feat(ring_theory/dedekind_finite) some ba...
Random Issue Bot (Feb 26 2021 at 14:20):
Today I chose PR 1822 for discussion!
[WIP] feat(ring_theory/dedekind_finite) some basics for dedekind finite rings
Created by @Alex J Best (@alexjbest) on 2019-12-22
Labels: WIP, merge-conflict, please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 11 2021 at 14:23):
Today I chose PR 1822 for discussion!
[WIP] feat(ring_theory/dedekind_finite) some basics for dedekind finite rings
Created by @Alex J Best (@alexjbest) on 2019-12-22
Labels: WIP, please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 06 2021 at 14:19):
Today I chose PR 1822 for discussion!
[WIP] feat(ring_theory/dedekind_finite) some basics for dedekind finite rings
Created by @Alex J Best (@alexjbest) on 2019-12-22
Labels: WIP, please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Alex J. Best (Dec 06 2021 at 14:48):
It would be nice to get this in to mathlib before the Lean 4 transition, but its not super high priority. I do have a branch refreshing this somewhere as it was discussed recently. And some of the pieces are making their way into mathlib independently (e.g. nilradicals).
Last updated: Dec 20 2023 at 11:08 UTC