pow_mul rational

Stream: new members

[Iocta]

import Mathlib
import Mathlib.Tactic

example (a : ℝ) (p q : ℚ) : a ^ (p + q) = a ^ p * a ^ q := by
/-
a : ℝ
p q : ℚ
⊢ sorryAx (Sort ?u.114130) true
-/

I guess it means "I don't know what type a ^ p is supposed to have"? What am I supposed to do?

[Mauricio Collares]

If you write "sorry" as the proof, Lean will say

failed to synthesize instance
  HPow ℝ ℚ ?m.91

flagging a problem with the theorem statement. Declaring p and q as reals is a valid fix, but it depends on what you want to do.

[Mauricio Collares]

To be able to prove it you'll probably have to assume that a is positive, though. See docs#Real.rpow_add

[Iocta]

So I can't even state the ℝ ℚ version of this?

[Kevin Buzzard]

What does $(-1)^{1/2}$ even mean here? Are you sure you can definitely assign a meaning to all those symbols which makes this always true?

[Kevin Buzzard]

You can only state it if you define what real^rational means. For example you could define r^q to mean r^(q regarded as real). Then it's unlikely to be true if r<0.

[Eric Wieser]

Though with that definition, $(-1)^{1/3} = -\frac{1}{2}$ which isn't exactly ideal

[Mauricio Collares]

Iocta said:

So I can't even state the ℝ ℚ version of this?

If you want, you can define your own power function taking a real and a rational, and write an HPow instance so notation works:

instance : HPow ℝ ℚ ℝ where
  hPow := yourFunction

But Mathlib doesn't provide such a definition out-of-the-box, so you will have to write a bunch of supporting lemmas yourself.

[Floris van Doorn]

Aside: the reason that Lean doesn't show a warning in the statement in the original code snippet is because there is a parse error in having an empty tactic block. This is a known bug: lean4#3556