Zulip Chat Archive

Stream: new members

Topic: arithmetic in ℝ


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Sep 30 2020 at 11:15):

Exciting! I am trying this out in place now.

view this post on Zulip 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