Reassociating docs#mul_opposite.op

Stream: Is there code for X?

[Yaël Dillies]

Is there a general set of typeclasses that implies (op b • a) • c = a • b • c? This is basically just a * (b * c) = a * b * c for scalar multiplication.

[Yaël Dillies]

Here's my use case

import data.set.pointwise.smul

open mul_opposite
open_locale pointwise

variables {α : Type*} [group α] {s t : set α} {a : α}

lemma set.singleton_mul' : {a} * s = a • s := set.singleton_mul
lemma set.mul_singleton' : s * {a} = op a • s := set.mul_singleton

example {a : α} : (op a • s) * t = s * a • t :=
by rw [←set.mul_singleton', ←set.singleton_mul', mul_assoc]

[Yaël Dillies]

@Eric Wieser, this question is probably yours.

[Eric Wieser]

I'm pretty sure it doesn't exist

[Eric Wieser]

Although I think I did make a thread suggesting it in the past

[Yaël Dillies]

The very long one with Jakob?

[Eric Wieser]

Either that one or one about actions on units

[Eric Wieser]

(op a • s) * t = s * a • t can be rewritten as op t • (op a • s) = op (a • t) • s = (a • op t) • s but that doesn't seem to help