# Zulip Chat Archive

## Stream: new members

### Topic: Scalar multiplication in modules

#### Adrián Doña Mateo (Dec 07 2020 at 22:02):

I am trying to get used to Z-modules in Lean but I am struggling to prove some simple stuff. I was hoping this could be done with `rfl`

or `simp`

.

```
import algebra.module.basic
example (a x y : ℤ) : a • (x, y) = (a * x, a * y) := sorry
```

#### Alex J. Best (Dec 07 2020 at 22:48):

Hmm this was slightly harder than you'd hope yes, maybe someone else can find an easier way:

```
example (a x y : ℤ) : a • (x, y) = (a * x, a * y) := begin
simp only [prod.smul_mk, prod.mk.inj_iff],
exact ⟨gsmul_int_int _ _, gsmul_int_int _ _⟩,
end
```

or as a calc mode

```
example (a x y : ℤ) : a • (x, y) = (a * x, a * y) := calc
a • (x , y) = (a • (x,y).1, a • (x,y).2) : by refl
... = (a * (x,y).1, a * (x,y).2) : by congr; exact gsmul_int_int _ _
```

#### Alex J. Best (Dec 07 2020 at 22:50):

Ah I think the problem is that mathlib is missing a lemma

```
@[simp]
lemma smul_int_int (a b : ℤ) : a • b = a * b := gsmul_int_int _ _
```

#### Yury G. Kudryashov (Dec 08 2020 at 05:13):

There are two "natural" instances for `has_scalar ℤ ℤ`

. One comes from docs#semiring.to_semimodule, and another one comes from docs#add_comm_group.int_module. Depending on the context, both can appear in goals.

#### Yury G. Kudryashov (Dec 08 2020 at 05:13):

For the first instance your identity would be a `rfl`

.

#### Eric Wieser (Dec 08 2020 at 07:18):

There are a few hints in `int_module`

that suggest the author thinks it may have been a bar idea. Is it preferable to use `•ℤ`

instead of that instance?

#### Adrián Doña Mateo (Dec 08 2020 at 11:36):

So adding something like `local attribute [instance, priority 1000] semiring.to_semimodule`

should make it `rfl`

then, right?

Last updated: Dec 20 2023 at 11:08 UTC