mathlib documentation

data.real.irrational

Irrational real numbers

In this file we define a predicate irrational on , prove that the n-th root of an integer number is irrational if it is not integer, and that sqrt q is irrational if and only if rat.sqrt q * rat.sqrt q ≠ q ∧ 0 ≤ q.

We also provide dot-style constructors like irrational.add_rat, irrational.rat_sub etc.

def irrational  :
→ Prop

A real number is irrational if it is not equal to any rational number.

Equations
theorem irrational_iff_ne_rational (x : ) :
irrational x ∀ (a b : ), x a / b

Irrationality of roots of integer and rational numbers

theorem irrational_nrt_of_notint_nrt {x : } (n : ) (m : ) :
x ^ n = m(¬∃ (y : ), x = y)0 < nirrational x

If x^n, n > 0, is integer and is not the n-th power of an integer, then x is irrational.

theorem irrational_nrt_of_n_not_dvd_multiplicity {x : } (n : ) {m : } (hm : m 0) (p : ) [hp : fact (nat.prime p)] :
x ^ n = m(multiplicity p m).get _ % n 0irrational x

If x^n = m is an integer and n does not divide the multiplicity p m, then x is irrational.

theorem irrational_sqrt_of_multiplicity_odd (m : ) (hm : 0 < m) (p : ) [hp : fact (nat.prime p)] :

Adding/subtracting/multiplying by rational numbers

theorem irrational.add_cases {x y : } :

theorem irrational.of_rat_add (q : ) {x : } :

theorem irrational.rat_add (q : ) {x : } :

theorem irrational.of_add_rat (q : ) {x : } :

theorem irrational.add_rat (q : ) {x : } :

theorem irrational.of_neg {x : } :

theorem irrational.neg {x : } :

theorem irrational.sub_rat (q : ) {x : } :

theorem irrational.rat_sub (q : ) {x : } :

theorem irrational.of_sub_rat (q : ) {x : } :

theorem irrational.of_rat_sub (q : ) {x : } :

theorem irrational.mul_cases {x y : } :

theorem irrational.of_mul_rat (q : ) {x : } :

theorem irrational.mul_rat {x : } (h : irrational x) {q : } :
q 0irrational (x * q)

theorem irrational.of_rat_mul (q : ) {x : } :
irrational ((q) * x)irrational x

theorem irrational.rat_mul {x : } (h : irrational x) {q : } :
q 0irrational ((q) * x)

theorem irrational.of_mul_self {x : } :
irrational (x * x)irrational x

theorem irrational.div_cases {x y : } :

theorem irrational.of_rat_div (q : ) {x : } :

theorem irrational.of_one_div {x : } :
irrational (1 / x)irrational x

theorem irrational.of_pow {x : } (n : ) :
irrational (x ^ n)irrational x

theorem irrational.of_fpow {x : } (m : ) :
irrational (x ^ m)irrational x

@[simp]
theorem irrational_rat_add_iff {q : } {x : } :

@[simp]
theorem irrational_add_rat_iff {q : } {x : } :

@[simp]
theorem irrational_rat_sub_iff {q : } {x : } :

@[simp]
theorem irrational_sub_rat_iff {q : } {x : } :

@[simp]