## 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


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.smulis the smul from group_power file.

Last updated: May 08 2021 at 09:11 UTC