# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: A typeclass for `(r : R) (x y : A) : (r • x)*y = r • (x*y)`

#### Eric Wieser (Jan 13 2021 at 15:41):

This lemma exists as docs#smul_mul_assoc, but that requires `A`

to be an algebra.

This property also holds for `A = α →₀ R`

, but there can be no algebra instance on `α →₀ R`

because it has no `1`

.

#### Eric Wieser (Jan 13 2021 at 15:42):

So is there a typeclass that can be extracted from algebra that sits somewhere between `algebra`

and `semimodule`

?

#### Anne Baanen (Jan 13 2021 at 15:53):

I guess you can fake it with docs#is_scalar_tower combined with docs#smul_eq_mul?

#### Eric Wieser (Jan 13 2021 at 16:23):

Not if `R`

is not commutative I can't

#### Eric Wieser (Jan 13 2021 at 16:23):

But I guess I don't really care about that case

#### Eric Wieser (Jan 13 2021 at 16:27):

Can you give a sketch of the `is_scalar_tower`

solution? What I have right now is

```
import data.finsupp.pointwise
namespace finsupp
section
variables {α R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
@[simp] lemma mul_smul_comm (s : R) (x y : α →₀ A) :
x * (s • y) = s • (x * y) :=
by { ext, simp [←mul_assoc]}
@[simp] lemma smul_mul_assoc (r : R) (x y : α →₀ A) :
(r • x) * y = r • (x * y) :=
by { ext, simp }
end
end finsupp
```

What arguments are you suggesting I instantiate `is_scalar_tower`

with in order to avoid needing to define `finsupp.mul_smul_comm`

at all?

#### Anne Baanen (Jan 13 2021 at 18:02):

Eric Wieser said:

Can you give a sketch of the

`is_scalar_tower`

solution?

You are right, I can't really put anything together that works nicely. I guess the best is indeed to add a new class in between `semimodule`

and `algebra`

.

Last updated: May 07 2021 at 20:11 UTC