Scalar multiplication in modules

Stream: new members

[Adrián Doña Mateo]

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]

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]

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]

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]

For the first instance your identity would be a rfl.

[Eric Wieser]

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]

So adding something like local attribute [instance, priority 1000] semiring.to_semimodule should make it rfl then, right?