arithmetic in ℝ

Stream: new members

[Scott Morrison]

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]

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]

Exciting! I am trying this out in place now.

[Scott Morrison]

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