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