Zulip Chat Archive

Stream: triage

Topic: PR #15983: feat(algebra/monoid_algebra/no_zero_divisors):...

Random Issue Bot (Mar 07 2023 at 14:08):

Today I chose PR 15983 for discussion!

feat(algebra/monoid_algebra/no_zero_divisors): more no-zero divisors on add_monoid_algebras
Created by @damiano (@adomani) on 2022-08-10
Labels: WIP, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Aug 23 2023 at 14:07):

Today I chose PR 15983 for discussion!

feat(algebra/monoid_algebra/no_zero_divisors): more no-zero divisors on add_monoid_algebras
Created by @damiano (@adomani) on 2022-08-10
Labels: WIP, t-algebra, too-late

Is this PR still relevant? Any recent updates? Anyone making progress?

Damiano Testa (Aug 23 2023 at 14:48):

I'm glad you asked!

There are currently several mathlib4 PR open to get this merged:

  • #6723, the main PR, depending on...
    • #6751, to_additive support for naming -- no real dependency, other than automated naming;
    • #6752, adding IsLeftCancel instance on MulOpposites (merged, thanks Eric!);
    • #6753, just some golfing -- no real dependency, other than help to shorten the diff (merged, thanks Alex and Oliver!);
    • #6755, adding subsingleton and MulOpposites on UniqueProds.

Last updated: Dec 20 2023 at 11:08 UTC