ring help

Stream: mathlib4

[Bolton Bailey]

My understanding was that ring is supposed to solve goals like the following:

import Mathlib

example
    (B: Type)
    [Ring B]
    (f g: B) :
    f + 5 * f = 6 * f := by
  ring

But ring doesn't solve this. What is going wrong?

[David Renshaw]

It works if I change Ring to CommRing

[Bolton Bailey]

Ah yes, I forgot that it had to be commutative. Thanks.

[David Renshaw]

or CommSemiring

[Bolton Bailey]

There should really be an error message that says you are doing it wrong when your equation is not over a CommSemiring.

[Jireh Loreaux]

i'm surprised the AddCommMonoidWithOne part of of ring can't handle this. I actually think this is a bug.

[David Renshaw]

ah, apparently noncomm_ring exists. This works:

example
    (B: Type)
    [Ring B]
    (f: B) :
    f + 5 * f = 6 * f := by
  noncomm_ring

[Jireh Loreaux]

It does, but it's very stupid. See the implementation to realize it's just a bunch of simp lemmas (and abel)

[Bolton Bailey]

Thanks to @Jireh Loreaux for resolving this with #19763!