rational power

Stream: Is there code for X?

[Shi You]

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]

It's because it's not true:

example : (2^(1/2)) ^ 2 = 1 := rfl

Can you understand why?

[Shi You]

Yes. In the context of integers.

[Eric Rodriguez]

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]

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]

ahh, you need analysis.special_functions.complex.pow. I don't think there's a has_pow ℝ ℚ in Lean, sadly