## Stream: new members

### Topic: trying out a simp lemma

#### Damiano Testa (Apr 12 2021 at 02:52):

Dear All,

what constitutes a good test for trying out a simp lemma? I list below what comes to mind: is there any other "standard" test that you would do?

• Check that #lint is happy.
• Make sure that CI is successful with the simp tag.
• Check that the statement of the new simp lemma can be proven by simp only after you tag the lemma with simp.
• Modify the statement a bit, in such a way that simp "should prove it" and check that it does.

I have ticked all of the above, except that I am still waiting on CI to finish.

Anything else?

Thanks!

#### Damiano Testa (Apr 12 2021 at 02:52):

The reason for asking is I would like to tag the lemmas below with simp and Scott suggested to "try it out"!

import algebra.module.basic
import algebra.algebra.basic

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] [semimodule ℕ R] (m : ℕ) :
m • (1 : R) = ↑m :=
by rw [←nsmul_eq_smul, nsmul_eq_mul, mul_one]

@[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] [semimodule ℤ R] (m : ℤ) :
m • (1 : R) = ↑m :=
by rw [← gsmul_eq_smul, gsmul_eq_mul, mul_one]

@[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
m • (1 : A) = ↑m :=
by rw [algebra.smul_def, mul_one, ring_hom.eq_rat_cast]


#### Damiano Testa (Apr 12 2021 at 05:15):

PR #7166

CI was successful with the simp tag for the three lemmas!

#### Scott Morrison (Apr 12 2021 at 05:38):

(Also, this would be better in general than in new members)

Last updated: Dec 20 2023 at 11:08 UTC