# Zulip Chat Archive

## Stream: general

### Topic: cannot compute cube root

#### Formally Verified Waffle Maker (Oct 19 2020 at 23:09):

The line:

```
use 8^((1 : ℚ)/3),
```

in the code:

```
import data.real.basic
import tactic
open real
theorem eight_has_a_cube_root : ∃ n, n^3 = 8 :=
begin
use 8^((1 : ℚ)/3),
ring,
end
```

makes Lean complain:

```
failed to instantiate goal with (frozen_name has_pow.pow) 8 ((frozen_name has_div.div) (typed_expr (frozen_name rat) 1) 3)
```

Any help would be appreciated :smile:

#### Bryan Gin-ge Chen (Oct 19 2020 at 23:18):

The error message isn't very helpful here, but if you use the very similar tactic#existsi, you'll see the underlying problem:

```
import data.real.basic
import tactic
theorem eight_has_a_cube_root : ∃ n, n^3 = 8 :=
begin
existsi 8^((1 : ℚ)/3),
/-
failed to synthesize type class instance for
⊢ has_pow ℕ ℚ
state:
⊢ ∃ (n : ℕ), n ^ 3 = 8
-/
ring,
end
```

The problem is that Lean doesn't know how to raise a natural number to a rational power.

#### Floris van Doorn (Oct 19 2020 at 23:22):

Note that this works:

```
import analysis.special_functions.pow
open real
theorem eight_has_a_cube_root : ∃ n : ℝ, n^3 = 8 :=
begin
use 8^((1 : ℝ)/3),
end
```

#### Floris van Doorn (Oct 19 2020 at 23:23):

I've imported the function where docs#real.has_pow was defined, changed the statement to talk about reals (which I *think* is what you wanted?) and use a real exponent.

#### Floris van Doorn (Oct 19 2020 at 23:26):

Here is the rest of the proof (with 7 instead of 8):

```
import analysis.special_functions.pow
open real
theorem seven_has_a_cube_root : ∃ n : ℝ, n^3 = 7 :=
begin
use 7^((1 : ℝ)/3),
rw [← rpow_nat_cast, ← real.rpow_mul]; norm_num
end
```

#### Formally Verified Waffle Maker (Oct 20 2020 at 00:48):

Floris van Doorn said:

Here is the rest of the proof (with 7 instead of 8):

`import analysis.special_functions.pow open real theorem seven_has_a_cube_root : ∃ n : ℝ, n^3 = 7 := begin use 7^((1 : ℝ)/3), rw [← rpow_nat_cast, ← real.rpow_mul]; norm_num end`

Bryan Gin-ge Chen said:

The error message isn't very helpful here, but if you use the very similar tactic#existsi, you'll see the underlying problem:

`import data.real.basic import tactic theorem eight_has_a_cube_root : ∃ n, n^3 = 8 := begin existsi 8^((1 : ℚ)/3), /- failed to synthesize type class instance for ⊢ has_pow ℕ ℚ state: ⊢ ∃ (n : ℕ), n ^ 3 = 8 -/ ring, end`

The problem is that Lean doesn't know how to raise a natural number to a rational power.

Thank you very much for your kind support! :pray:

#### Kenny Lau (Oct 20 2020 at 07:05):

@Formally Verified Waffle Maker there's some basic type theory to be known here. in maths we have partial functions, and numbers have flexible types ($\Bbb N \subset \Bbb Z \subset \Bbb Q \subset \Bbb R \subset \Bbb C$). but in Lean, a natural number cannot suddenly become a real number, so expressions like $8^{1/3}$ doesn't make sense (or at least shouldn't give you a natural number) because it would have to be defined for all natural numbers, and last time I checked $7^{1/3}$ is not a natural number. Here's the thing. Functions have fixed types as well. A function (such as cube root) have a fixed type for the input and a fixed type for the output (technically a lie, but let's go with this for now), so cube root has to have codomain $\Bbb R$.

Last updated: Dec 20 2023 at 11:08 UTC