# Zulip Chat Archive

## Stream: new members

### Topic: nat.cast_smul

#### Joe (Aug 12 2019 at 13:50):

I tried to find a proof for `(n:ℝ) • x = n • x`

but failed. I wrote a proof myself.

Should I PR this?

import algebra.module variables {α : Type*} {β : Type*} [semiring α] [add_comm_monoid β] [semimodule α β] namespace nat @[simp, elim_cast] lemma cast_smul (b : β) : ∀n:ℕ, (n:α) • b = n • b | 0 := by simp | (n + 1) := by simp [add_smul, cast_smul] end nat

#### Mario Carneiro (Aug 12 2019 at 14:01):

looks good to me

#### Mario Carneiro (Aug 12 2019 at 14:03):

what is the smul on the right? Is that the one from group_power?

#### Reid Barton (Aug 12 2019 at 14:04):

The one on the left is from `semimodule`

#### Reid Barton (Aug 12 2019 at 14:06):

For the one on the right I think any `add_comm_monoid`

gets a `semimodule nat`

instance--that name sounds plausible

#### Mario Carneiro (Aug 12 2019 at 14:07):

do we have a `semimodule nat B`

instance? The group_power file defines a `has_scalar`

instance directly

#### Mario Carneiro (Aug 12 2019 at 14:07):

but it may have upgraded it to a semimodule for an appropriate structure on B

#### Reid Barton (Aug 12 2019 at 14:07):

I wonder whether this should really be a simp lemma. In the sensitivity conjecture formalization we specifically needed the one on the left, and it was already slightly nonobvious how to write it

#### Reid Barton (Aug 12 2019 at 14:08):

Ah, I don't know whether that `semimodule nat`

instance actually exists in mathlib

#### Mario Carneiro (Aug 12 2019 at 14:09):

I think these are usually simp lemmas; the cast tactic is supposed to handle "fighting simp" in these sorts of cases

#### Joe (Aug 12 2019 at 14:29):

I found `add_comm_monoid.semimodule`

in the library. It shows `semimodule ℕ β`

.

So maybe it is useful to add another `cast_smul`

?

lemma cast_smul' (b : β) : ∀n:ℕ, (n:α) • b = add_monoid.smul n b

where `add_monoid.smul`

is the smul from group_power file.

Last updated: May 08 2021 at 09:11 UTC