A question about type mistakes

Stream: maths

[Move fast]

      have h2 :((((1 : ℝ )+((2 : ℝ) ^ ((1 : ℝ) / 3) )))^((1 : ℝ) / 2): ℝ)^(6:ℕ )=(((1 : ℝ )+((2 : ℝ) ^ ((1 : ℝ) / 3) )))^(3:ℕ )   := by
        rw [← h0]
        have h_01 : 0 < (2:ℝ) :=
          by norm_num
        have h_02 : 0 < (2 : ℝ) ^ ((1 : ℝ) / 3) :=
          by apply Real.rpow_pos_of_pos h_01 ((1 : ℝ) / 3)
        have h_03 : 0 < (1:ℝ) :=
          by norm_num
        have h_04 : 0 < (1 : ℝ )+(2 : ℝ) ^ ((1 : ℝ) / 3) :=
          by apply add_pos h_03 h_02
        have h_05 : 0 ≤  (1 : ℝ )+(2 : ℝ) ^ ((1 : ℝ) / 3) :=
          by apply h_04.le
        rw [← Real.rpow_mul_natCast h_05]
        norm_num
        rw [← Real.rpow_mul_natCast h_05]
        norm_num
        rfl

image.png
How can I solve this problem? Did you meet this question before?

[Aaron Liu]

docs#Real.rpow_natCast

[Move fast]

Thank you very much!

[Move fast]

If I want to express \sqrt{i} in Lean 4, how can I do?
image.png

[Aaron Liu]

Which square root of i?

[Ruben Van de Velde]

What is a square root?

[Move fast]

We can define that $(\sqrt i)^2=i$. However, I don't know if it is appropriate.
In Lean, we can see that it must be a real number in a sqaure root.

[Move fast]

image.png
I have already found its definition, by Euler formula.

[Yury G. Kudryashov]

@Move fast Please answer some simple questions before we continue this discussion.

• What's your math background?
• Did you complete any Lean intro course (e.g., the Natural Numbers Game)?
• Have you read Math in Lean?
• You ask many questions on assorted topics. Where do they come from? I mean, why are you interested in these particular problems?
• Do you use external tools (e.g., AI) to generate/adjust your lean code?
• Do you have a reason to use a nickname instead of a real world name? Generally, we prefer real world names in this Zulip.

[Arthur Rats]

@Yury G. Kudryashov the Natural number game is valid for start in intro of lean? i,m in start and want know more about this.

[Kyle Miller]

Yes, many of us started with Lean using the Natural Number Game. (I did!)

[suhr]

Do you have a reason to use a nickname instead of a real world name? Generally, we prefer real world names in this Zulip.

I really hope this is not a requirement.

[Mauricio Collares]

It's not a requirement, and the moderators always take care to use expressions such as "We strongly prefer".

[Move fast]

I'm an undergraduate student and I'm studying MIL. I have learned some abstract algebra (more of group theory) and number theory. So I have chosen some simple questions from these books and I'm trying to solve them. At first, I used LLM to learn lean, but it didn't seem like a good idea. Therefore, I start to study MIL now. I don't have an English name, but I hope I can move faster on the path of learning Lean. So that is my nick name.

[Yury G. Kudryashov]

Thank you for the answer.