Zulip Chat Archive

Stream: new members

Topic: nat.cast_smul


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2019 at 14:01):

looks good to me

view this post on Zulip Mario Carneiro (Aug 12 2019 at 14:03):

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

view this post on Zulip Reid Barton (Aug 12 2019 at 14:04):

The one on the left is from semimodule

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2019 at 14:07):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2019 at 14:08):

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

view this post on Zulip 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

view this post on Zulip 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