## Stream: new members

### Topic: arithmetic in ℝ

#### Scott Morrison (Sep 30 2020 at 10:50):

Could someone put me out of my misery here?

import analysis.special_functions.pow

local notation √2 := (2^(2⁻¹ : ℝ) : ℝ)

example : √2 * √2 ^ 3 = √2 * (2 * √2⁻¹ + 4 * (√2⁻¹ * 2⁻¹)) :=
sorry


#### Shing Tak Lam (Sep 30 2020 at 11:11):

This works, but the proof isn't great

import analysis.special_functions.pow
import tactic

local notation √2 := (2^(2⁻¹ : ℝ) : ℝ)

-- This should be in mathlib, somewhere, right?
lemma rpow_eq_pow_cast (a : ℝ) (n : ℕ) : a ^ (n : ℝ) = a ^ n := by norm_num

example : √2 * √2 ^ 3 = √2 * (2 * √2⁻¹ + 4 * (√2⁻¹ * 2⁻¹)) :=
begin
ring,
rw [mul_assoc, inv_mul_cancel, ←rpow_eq_pow_cast, ←real.rpow_mul],
{ norm_num,
rw show (2 : ℝ) ^ (2 : ℝ) = (2 : ℝ) ^ (2 : ℕ), by { rw ←rpow_eq_pow_cast, norm_num },
norm_num },
{ norm_num },
{ -- I didn't find rpow_ne_zero
apply ne_of_gt,
apply real.rpow_pos_of_pos,
norm_num },
end


#### Scott Morrison (Sep 30 2020 at 11:15):

Exciting! I am trying this out in place now.

#### Scott Morrison (Sep 30 2020 at 11:28):

Works beautifully, thank you very much @Shing Tak Lam. I will add you name to the authors of the file I'm working on. :-)

Last updated: May 15 2021 at 22:14 UTC