roots of quadratic polynomial

Stream: new members

[tsuki]

How to slove the problem without using Real.quadratic_eq_zero_iff, I want to introduce a lemma that the polynomial has only two roots. But not sure how to write it. Maybe use Polynomial.card_roots

lemma calc_by_sympy :  (3:ℕ) * b ^ 2 + 2 * b + 1 = 57 →  b = 4 ∨ b = (-14/3:ℝ) := by
  intro h

[Jireh Loreaux]

This isn't a #mwe. I don't know what is the type of b.

[tsuki]

sorry, this is the complete statement

import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

lemma calc_by_sympy :  (3:ℕ) * b ^ 2 + 2 * b + 1 = 57 →  b = 4 ∨ b = (-14/3:ℝ) := by
  intro h
  have l₁ :  (3:ℕ) * 4 ^ 2 + 2 * 4 + 1 = 57 := by
    ring
  have l₂ : (3:ℕ) * (-14/3:ℝ) ^ 2 + 2 * (-14/3:ℝ) + 1 = 57 := by
    ring
  sorry

[Ilmārs Cīrulis]

How do you solve quadratic equation on paper?

[Ilmārs Cīrulis]

I cleared a bit up, I believe. Aesop not needed here, imo, same with anything else, except open Real probably.

import Mathlib
open Real

lemma T (b: ℝ): 3 * b ^ 2 + 2 * b + 1 = 57 → b = 4 ∨ b = - 14 / 3 := by
  sorry

[Ilmārs Cīrulis]

l₁ and l₂ is useful only if you want to prove implication in both directions (iff or ↔). Then they could be used, when proving direction from right to left.
Ok, they show, that 4 and (-14/3) are both roots of the quadratic equation. And quadratic equation can have only no more than two different roots. So there could be way to prove the theorem this way, too. Somehow.

[Edit:] Sorry, I was too sleepy. That's what the OP wrote about in the original post.

[Ilmārs Cīrulis]

Anyway, it's possible I learned new thing today.
Is it correct that open Real makes Lean to interpret all numerals as real numbers by default?

[Ilmārs Cīrulis]

School method required 18 lines in total (for me) and it's possible to golf it even much shorter, i believe.

[Ilmārs Cīrulis]

11 lines, when I used semicolons

[Wang Jingting]

import Mathlib
open Real

lemma T (b: ℝ): 3 * b ^ 2 + 2 * b + 1 = 57 → b = 4 ∨ b = - 14 / 3 := fun h ↦ by
  have : 3 * (b - 4) * (b - (- 14 / 3)) + 57 = 57 := by
    nth_rw 2 [← h]
    ring
  simpa [sub_eq_zero] using this

I think this works.

[tsuki]

Can you tell me what :=fun h means?

[Kevin Buzzard]

It's intro h but in term mode not tactic mode (before the by)

[Ruben Van de Velde]

Ilmārs Cīrulis said:

Anyway, it's possible I learned new thing today.
Is it correct that open Real makes Lean to interpret all numerals as real numbers by default?

No, it isn't

[Ilmārs Cīrulis]

Aha, it keeps exponents natural numbers, it seems. Smth like that?
At least that's what I see when I click on numbers.

[Kevin Buzzard]

Lean is inferring the types of numerals in a way which is unchanged by open Real

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

I tried to realise the idea of the original post about Polynomial.card_roots (as I understood it)... :sweat_smile:

I got stuck, though. Can someone help to finish the proof?
I finished it.

import Mathlib
open Real Polynomial

noncomputable def P: ℝ[X] := C 3 * X ^ 2 + C 2 * X - C 56

lemma T: P.roots = { 4, -14/3 } := by
  have HP: P ≠ 0 := by
    intro H0
    have H1: P.eval 1 = - 51 := by
      unfold P; simp; norm_num
    rw [H0] at H1; simp at H1
  have H0 := Polynomial.card_roots HP
  have H1: P.degree = 2 := by
    unfold P
    rw [Polynomial.degree_sub_eq_left_of_degree_lt]
    . rw [Polynomial.degree_add_eq_left_of_degree_lt]
      . simp
      . simp
    . simp
      rw [Polynomial.degree_add_eq_left_of_degree_lt]
      . simp
      . simp
  rw [H1] at H0
  simp at H0
  have H3: 4 ∈ P.roots := by
    simp [HP]
    unfold P; simp; norm_num
  have H4: - 14 / 3 ∈ P.roots := by
    simp [HP]
    unfold P; simp; norm_num
  have H5: {4, -14/3} ⊆ P.roots := by
    intro x Hx; simp at Hx
    obtain Hx | Hx := Hx <;> subst x <;> assumption
  refine Eq.symm (Multiset.eq_of_le_of_card_le ?_ H0)
  rw [Multiset.le_iff_subset]; assumption
  simp; norm_num

[tsuki]

wow, it's amazing!!!

[Ilmārs Cīrulis]

It probably isn't, i'm very much beginner who just jumps around the place in hyperactive way.

[Ilmārs Cīrulis]

Still, it was fun to write, in the way of formal proofs. :sweat_smile:

[Michael Rothgang]

For once, the compute_degree tactic looks like it could be useful for H1.