## 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: May 11 2021 at 12:15 UTC