irrational

Stream: new members

[vxctyxeha]

I want to prove that the square root of 2 plus the square root of 7 is an irrational number, and I found add_cases: Irrational (x + y) → Irrational x ∨ Irrational y in mathlib; however, I tried using rw [add_case], but it failed.·

import Mathlib
open Polynomial
namespace Irrational
theorem sqrt2_add_sqrt7_irrational : Irrational (Real.sqrt 2 + Real.sqrt 7) := by
  rw [add_cases]

[Sébastien Gouëzel]

What is your math proof?

[Aaron Liu]

You can't rewrite because it's not an iff

[Aaron Liu]

Compare with

import Mathlib
open Polynomial
namespace Irrational
theorem sqrt2_add_neg_sqrt2_irrational : Irrational (Real.sqrt 2 + -Real.sqrt 2) := by
  rw [add_cases]

[vxctyxeha]

Is there a definition of Isrational in mathlib?

[Kevin Buzzard]

I don't believe so, just use Exists q : Rat, r = q.

[Notification Bot]

vxctyxeha has marked this topic as resolved.

[Notification Bot]

vxctyxeha has marked this topic as unresolved.

[vxctyxeha]

By the way, do you have any suggestions for proving that e is an irrational number?

[Eric Wieser]

#new members > Euler number (Real.exp 1) is transcendental @ 💬