nat.cast_smul

Stream: new members

[Joe]

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]

looks good to me

[Mario Carneiro]

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

[Reid Barton]

The one on the left is from semimodule

[Reid Barton]

For the one on the right I think any add_comm_monoid gets a semimodule nat instance--that name sounds plausible

[Mario Carneiro]

do we have a semimodule nat B instance? The group_power file defines a has_scalar instance directly

[Mario Carneiro]

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

[Reid Barton]

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]

Ah, I don't know whether that semimodule nat instance actually exists in mathlib

[Mario Carneiro]

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

[Joe]

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.