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 and linarith.

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