## Stream: maths

### Topic: dirty nom_cast

#### Patrick Massot (Sep 21 2019 at 20:02):

@Paul-Nicolas Madelaine and @Rob Lewis do you know how I could clean the following two lemmas:

@[simp, move_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q) (k : ℤ) :
((q ^ k : ℚ) : α) = q ^ k :=
begin
cases k,
{ erw fpow_of_nat,
rw rat.cast_pow,
erw fpow_of_nat },
{ rw fpow_neg_succ_of_nat,
rw fpow_neg_succ_of_nat,
norm_cast }
end

lemma num_aux (p : ℕ) (n : ℤ) :  (coe : ℚ → ℝ) ((p : ℚ) ^ n) = (p : ℝ) ^ n :=
begin
rw cast_fpow,
congr' 1,
norm_cast
end


#### Rob Lewis (Sep 23 2019 at 08:08):

@[simp, elim_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q : ℚ) (k : ℤ) :
((q ^ k : ℚ) : α) = q ^ k :=
begin
cases k,
{ erw [fpow_of_nat, rat.cast_pow, fpow_of_nat] },
{ simp only [fpow_neg_succ_of_nat], norm_cast }
end

lemma num_aux (p : ℕ) (n : ℤ) :  (coe : ℚ → ℝ) ((p : ℚ) ^ n) = (p : ℝ) ^ n :=
begin
norm_cast
end


Not sure right now why the erw is needed there, but whatever makes rw and simp fail is probably also making norm_cast fail.

#### Floris van Doorn (Sep 23 2019 at 15:45):

The problem is that fpow_of_nat is stated using (coe : ℕ → ℤ), while in the goal we have int.of_nat which are not syntactically equal. This works:

@[simp] lemma fpow_of_nat' {α} [division_ring α] (a : α) (n : ℕ) : a ^ int.of_nat n = a ^ n := rfl

@[simp, elim_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q : ℚ) (k : ℤ) :
((q ^ k : ℚ) : α) = q ^ k :=
by cases k; simp [fpow_neg_succ_of_nat]


#### Floris van Doorn (Sep 23 2019 at 15:47):

Although the actual missing simp lemma is that int.of_nat should be turned into a coercion:

@[simp] lemma of_nat_eq_coe (n : ℕ) : int.of_nat n = n := rfl


Last updated: May 09 2021 at 09:11 UTC