Real numbers

Stream: general

[Jim Stuttard]

My first attempt at a proof in leanprover online:
theorem quadratic_formula :
∀ (a b c : ℝ), a ≠ 0 →
∃ (x₁ x₂ : ℝ),
x₁ + x₂ = -b / a ∧ x₁ * x₂ = c / a :=
begin
intros a b c ha,
have hb : b ≠ 0,
{ rw [ne.def, ← sub_eq_zero],
apply mul_ne_}
end
Gives the errors "Unknown identifiers 'R'". How do I enter the gothic R for real numbers?

[Eric Wieser]

Can you edit your message to use #backticks?

[Eric Wieser]

And is that your full code, or did you have some import lines too?

[Johan Commelin]

@Jim Stuttard You should probably have something like import data.real.basic at the top of your file.

[Jim Stuttard]

PS I'm on Ubuntu but haven't manage to install lean4-mode in emacs yet.

[Johan Commelin]

Your code looks more like Lean 3 than Lean 4.

[Kevin Buzzard]

Jim read about how to write an #mwe because if you follow the instructions there it's much easier to help you.

[Kevin Buzzard]

By the way your theorem is not true -- if the quadratic has no real roots then you won't be able to find x_1 and x_2. You could fix this by e.g. switching to $\mathbb{C}$.

[Michael Stoll]

... and there is no reason for b to be nonzero ...

[Jim Stuttard]

Johan I'm using the online prover which iiuc is Lean3. Tnx for your suggestions Kevin and Michael. This was an overambitious attempt. Will do.