The "other kind" of commutator

Stream: Is there code for X?

[Robert Maxton]

Is there code anywhere for ring commutators? [a,b] = a b - b a, and using such to simplify/normalize expressions.

[Oliver Nash]

Possibly you're looking for docs#ring.has_bracket

[Oliver Nash]

You might find the noncomm_ring tactic useful if that's right.

[Robert Maxton]

Yep, that was it. Thanks!

[Thomas Browning]

@Oliver Nash One thing we need to think about eventually is a looming conflict between additive group commutators and ring commutators. This conflict is why the commutator portion of the group theory library is just stated multiplicatively.

[Oliver Nash]

Is there definitely a conflict though? I realise we use the same word and typeclass but they're mathematically different things. Are there actually situations where we want additive group commutators?

[Thomas Browning]

Probably not, but it just means that any group theory result relying on commutators can't be easily additivized. Probably not an issue though, since additive groups tend to be abelian.