sqrt type

Stream: new members

[vxctyxeha]

function expected at
sqrt
term has type
?m.479

import Mathlib

open Polynomial Complex


theorem roots_of_x4_plus_3x_plus_3 :
  {x : ℂ | x ^ 4 + 3 * x + 3 = 0} =
  { ((I * (Real.sqrt 3) + sqrt (3 + 2 * (Real.sqrt 3) * I)) / 2),
    ((I * (Real.sqrt 3) - sqrt (3 + 2 * (Real.sqrt 3) * I)) / 2),
    ((-I * (Real.sqrt 3) + sqrt (3 - 2 * (Real.sqrt 3) * I)) / 2),
    ((-I * (Real.sqrt 3) - sqrt (3 - 2 * (Real.sqrt 3) * I)) / 2) } := by

[Aaron Liu]

That's because the sqrt function doesn't exist.

[Aaron Liu]

Can I ask what you were intending to formalize?

[Robin Arnez]

I think complex square root is just x ^ (1/2), not sure if there's a better way

[vxctyxeha]

Aaron Liu said:

That's because the sqrt function doesn't exist.

find all complex roots

[Aaron Liu]

So there are two options I can think of right now, which are you can state it "for all square roots of $\frac32\pm i\sqrt3$" or you can just write it as x ^ (2⁻¹)

[vxctyxeha]

image.png
why does it lead to Obvious mistake after use simp(/user_uploads/3121/c1cVqYntOpUSToUHirZMa76X/image.png)

import Mathlib

open Polynomial Complex


noncomputable section

theorem roots_of_x4_plus_3x_plus_3_ref_style :

      {x : ℂ | x ^ 4 + 3 * x + 3 = 0} =

      { ((I * (Real.sqrt 3) +  (3 + 2 * (Real.sqrt 3) * I))^(1/2) / 2),

        ((I * (Real.sqrt 3) -  (3 + 2 * (Real.sqrt 3) * I))^(1/2) / 2),

        ((-I * (Real.sqrt 3) +  (3 - 2 * (Real.sqrt 3) * I))^(1/2) / 2),

        ((-I * (Real.sqrt 3) -  (3 - 2 * (Real.sqrt 3) * I))^(1/2) / 2) } := by

  ext x; simp only [Set.mem_setOf_eq, Set.mem_insert_iff, Set.mem_singleton_iff]

  have h_fac_full : x ^ 4 + 3 * x + 3 =

    (x - ((I * (Real.sqrt 3) +  (3 + 2 * (Real.sqrt 3) * I))^(1/2) / 2)) *

    (x - ((I * (Real.sqrt 3) -  (3 + 2 * (Real.sqrt 3) * I)) ^(1/2)/ 2)) *

    (x - ((-I * (Real.sqrt 3) +  (3 - 2 * (Real.sqrt 3) * I))^(1/2) / 2)) *

    (x - ((-I * (Real.sqrt 3) - (3 - 2 * (Real.sqrt 3) * I)) ^(1/2)/ 2)) := by

    have h_p_fac : x ^ 4 + 3 * x + 3 =

      (x ^ 2 - I * (Real.sqrt 3) * x - (3 / 2 + I * (Real.sqrt 3) / 2)) *

      (x ^ 2 + I * (Real.sqrt 3) * x - (3 / 2 - I * (Real.sqrt 3) / 2)) := by

      ring_nf;simp

      have add: (ofReal √3 : ℂ) ^ 2 = 3 := by norm_cast; simp only [Nat.ofNat_nonneg, Real.sq_sqrt]

      rw [add];ring_nf

    have h_q1_fac : x ^ 2 - I * (Real.sqrt 3) * x - (3 / 2 + I * (Real.sqrt 3) / 2)

                    = (x - ((I * (Real.sqrt 3) +  (3 + 2 * (Real.sqrt 3) * I))^(1/2) / 2)) *

                      (x - ((I * (Real.sqrt 3) -  (3 + 2 * (Real.sqrt 3) * I)) ^(1/2)/ 2)) := by

      simp

[Aaron Liu]

That's because the prompt you typed into Wolfram Alpha is not the same as what you wrote in Lean.

[vxctyxeha]

(deleted)