Zulip Chat Archive
Stream: Is there code for X?
Topic: rational power
Shi You (Dec 02 2021 at 12:03):
Is there a tactic to compute the rational power of a number?
example : (2^(1/2)) ^ 2 = 2 := by library_search
The library_search tactic failed to give a result.
Sebastien Gouezel (Dec 02 2021 at 12:11):
It's because it's not true:
example : (2^(1/2)) ^ 2 = 1 := rfl
Can you understand why?
Shi You (Dec 02 2021 at 12:17):
Yes. In the context of integers.
Eric Rodriguez (Dec 02 2021 at 12:18):
for this specific example, (with the correct modifications to the cast), you can do it with this:
example : (2^(1/2 : ℝ) : ℝ) ^ 2 = 2 :=
begin
rw [←real.rpow_nat_cast, ←real.rpow_mul]; simp
end
But I don't think there'll be a general-purpose tactic; closest things may be norm_num
and linarith
.
Shi You (Dec 02 2021 at 12:20):
Eric Rodriguez said:
for this specific example, (with the correct modifications to the cast), you can do it with this:
example : (2^(1/2 : ℝ) : ℝ) ^ 2 = 2 := begin rw [←real.rpow_nat_cast, ←real.rpow_mul]; simp end
But I don't think there'll be a general-purpose tactic; closest things may be
norm_num
andlinarith
.
I got this error from your code:
failed to synthesize type class instance for
⊢ has_pow ℝ ℝ
Eric Rodriguez (Dec 02 2021 at 12:25):
ahh, you need analysis.special_functions.complex.pow
. I don't think there's a has_pow ℝ ℚ
in Lean, sadly
Last updated: Dec 20 2023 at 11:08 UTC