## 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