smul casting

Stream: new members

[Jalex Stark]

I think the following is true and should follow easily from the library but I don't yet have a clue about the proof:

example (d : ℕ) : (d : ℤ) = d • (1 : ℤ) := sorry

[Jalex Stark]

here's an induction proof

local attribute [simp]
lemma nat.smul_one (d : ℕ) : d • (1 : ℤ) = (d : ℤ) :=
begin
  induction d with k hk, simp,
  rw nat.succ_eq_add_one, push_cast,
  rw ← hk, rw add_smul, simp,
end

[Jalex Stark]

this feels like a simp lemma? \Z should generalize to an arbitrary ring?

[Kevin Buzzard]

Yeah maybe there should be some smul_one simp lemma in some generality.

[Jalex Stark]

I'll take that as evidence that using local attribute [simp] in my local project is not a terrible choice

[Jalex Stark]

oh my proof already works for generalizing integers to rings

[Jalex Stark]

local attribute [simp]
lemma nat.smul_one (d : ℕ) (R : Type*) [ring R] : d • (1 : R) = (d : R) :=
begin
  induction d with k hk, simp,
  rw nat.succ_eq_add_one, push_cast,
  rw ← hk, rw add_smul, simp,
end

[Kevin Buzzard]

There was some change recently about some other smul involving naturals, I guess someone who understands that will know whether this affects what's going on here