feat(algebra/algebra/basic algebra/module/basic): add 3 lemmas m • (1…

… : R) = ↑m (#7094)

Three lemmas asserting `m • (1 : R) = ↑m`, where `m` is a natural number, an integer or a rational number.

Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.60smul_one_eq_coe.60

  Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/algebra/algebra/basic.lean

@@ -609,6 +609,10 @@ variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 @[simp] lemma map_div (x y) : φ (x / y) = φ x / φ y :=
 φ.to_ring_hom.map_div x y
 
+lemma rat.smul_one_eq_coe [algebra ℚ A] (m : ℚ) :
+  m • (1 : A) = ↑m :=
+by rw [algebra.smul_def, mul_one, ring_hom.eq_rat_cast]
+
 end division_ring
 
 theorem injective_iff {R A B : Type*} [comm_semiring R] [ring A] [semiring B]

src/algebra/module/basic.lean

@@ -576,3 +576,11 @@ end no_zero_smul_divisors
 -- We finally turn on these instances globally. By doing this here, we ensure that none of the
 -- lemmas about nat semimodules above are specific to these instances.
 attribute [instance] add_comm_monoid.nat_semimodule add_comm_group.int_module
+
+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]
+
+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]