# mathlibdocumentation

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 (x : ) :
Prop

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

Equations
Instances for irrational
theorem irrational_iff_ne_rational (x : ) :
∀ (a b : ), x a / b
theorem transcendental.irrational {r : } (tr : r) :

A transcendental real number is irrational.

### Irrationality of roots of integer and rational numbers #

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

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)] (hxr : x ^ n = m) (hv : m).get _ % n 0) :

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)] (Hpv : m).get _ % 2 = 1) :
theorem nat.prime.irrational_sqrt {p : } (hp : nat.prime p) :
theorem irrational_sqrt_two  :

Irrationality of the Square Root of 2

theorem irrational_sqrt_rat_iff (q : ) :
q 0 q
@[protected, instance]
def irrational.decidable (q : ) :
Equations

### Dot-style operations on irrational#

#### Irrational number is not equal to a rational/integer/natural number #

theorem irrational.ne_rat {x : } (h : irrational x) (q : ) :
x q
theorem irrational.ne_int {x : } (h : irrational x) (m : ) :
x m
theorem irrational.ne_nat {x : } (h : irrational x) (m : ) :
x m
theorem irrational.ne_zero {x : } (h : irrational x) :
x 0
theorem irrational.ne_one {x : } (h : irrational x) :
x 1
@[simp]
theorem rat.not_irrational (q : ) :
@[simp]
theorem int.not_irrational (m : ) :
@[simp]
theorem nat.not_irrational (m : ) :

#### Addition of rational/integer/natural numbers #

theorem irrational.add_cases {x y : } :
irrational (x + y)

If x + y is irrational, then at least one of x and y is irrational.

theorem irrational.of_rat_add (q : ) {x : } (h : irrational (q + x)) :
theorem irrational.rat_add (q : ) {x : } (h : irrational x) :
theorem irrational.of_add_rat (q : ) {x : } :
irrational (x + q)
theorem irrational.add_rat (q : ) {x : } (h : irrational x) :
theorem irrational.of_int_add {x : } (m : ) (h : irrational (m + x)) :
theorem irrational.of_add_int {x : } (m : ) (h : irrational (x + m)) :
theorem irrational.int_add {x : } (h : irrational x) (m : ) :
theorem irrational.add_int {x : } (h : irrational x) (m : ) :
theorem irrational.of_nat_add {x : } (m : ) (h : irrational (m + x)) :
theorem irrational.of_add_nat {x : } (m : ) (h : irrational (x + m)) :
theorem irrational.nat_add {x : } (h : irrational x) (m : ) :
theorem irrational.add_nat {x : } (h : irrational x) (m : ) :

#### Negation #

theorem irrational.of_neg {x : } (h : irrational (-x)) :
@[protected]
theorem irrational.neg {x : } (h : irrational x) :

#### Subtraction of rational/integer/natural numbers #

theorem irrational.sub_rat (q : ) {x : } (h : irrational x) :
theorem irrational.rat_sub (q : ) {x : } (h : irrational x) :
theorem irrational.of_sub_rat (q : ) {x : } (h : irrational (x - q)) :
theorem irrational.of_rat_sub (q : ) {x : } (h : irrational (q - x)) :
theorem irrational.sub_int {x : } (h : irrational x) (m : ) :
theorem irrational.int_sub {x : } (h : irrational x) (m : ) :
theorem irrational.of_sub_int {x : } (m : ) (h : irrational (x - m)) :
theorem irrational.of_int_sub {x : } (m : ) (h : irrational (m - x)) :
theorem irrational.sub_nat {x : } (h : irrational x) (m : ) :
theorem irrational.nat_sub {x : } (h : irrational x) (m : ) :
theorem irrational.of_sub_nat {x : } (m : ) (h : irrational (x - m)) :
theorem irrational.of_nat_sub {x : } (m : ) (h : irrational (m - x)) :

#### Multiplication by rational numbers #

theorem irrational.mul_cases {x y : } :
irrational (x * y)
theorem irrational.of_mul_rat (q : ) {x : } (h : irrational (x * q)) :
theorem irrational.mul_rat {x : } (h : irrational x) {q : } (hq : q 0) :
theorem irrational.of_rat_mul (q : ) {x : } :
irrational (q * x)
theorem irrational.rat_mul {x : } (h : irrational x) {q : } (hq : q 0) :
theorem irrational.of_mul_int {x : } (m : ) (h : irrational (x * m)) :
theorem irrational.of_int_mul {x : } (m : ) (h : irrational (m * x)) :
theorem irrational.mul_int {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.int_mul {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.of_mul_nat {x : } (m : ) (h : irrational (x * m)) :
theorem irrational.of_nat_mul {x : } (m : ) (h : irrational (m * x)) :
theorem irrational.mul_nat {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.nat_mul {x : } (h : irrational x) {m : } (hm : m 0) :

#### Inverse #

theorem irrational.of_inv {x : } (h : irrational x⁻¹) :
@[protected]
theorem irrational.inv {x : } (h : irrational x) :

#### Division #

theorem irrational.div_cases {x y : } (h : irrational (x / y)) :
theorem irrational.of_rat_div (q : ) {x : } (h : irrational (q / x)) :
theorem irrational.of_div_rat (q : ) {x : } (h : irrational (x / q)) :
theorem irrational.rat_div {x : } (h : irrational x) {q : } (hq : q 0) :
theorem irrational.div_rat {x : } (h : irrational x) {q : } (hq : q 0) :
theorem irrational.of_int_div {x : } (m : ) (h : irrational (m / x)) :
theorem irrational.of_div_int {x : } (m : ) (h : irrational (x / m)) :
theorem irrational.int_div {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.div_int {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.of_nat_div {x : } (m : ) (h : irrational (m / x)) :
theorem irrational.of_div_nat {x : } (m : ) (h : irrational (x / m)) :
theorem irrational.nat_div {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.div_nat {x : } (h : irrational x) {m : } (hm : m 0) :
theorem irrational.of_one_div {x : } (h : irrational (1 / x)) :

#### Natural and integerl power #

theorem irrational.of_mul_self {x : } (h : irrational (x * x)) :
theorem irrational.of_pow {x : } (n : ) :
irrational (x ^ n)
theorem irrational.of_zpow {x : } (m : ) :
irrational (x ^ m)
theorem one_lt_nat_degree_of_irrational_root (x : ) (p : polynomial ) (hx : irrational x) (p_nonzero : p 0) (x_is_root : p = 0) :

### Simplification lemmas about operations #

@[simp]
theorem irrational_rat_add_iff {q : } {x : } :
@[simp]
theorem irrational_int_add_iff {m : } {x : } :
@[simp]
theorem irrational_nat_add_iff {n : } {x : } :
@[simp]
theorem irrational_add_rat_iff {q : } {x : } :
@[simp]
theorem irrational_add_int_iff {m : } {x : } :
@[simp]
theorem irrational_add_nat_iff {n : } {x : } :
@[simp]
theorem irrational_rat_sub_iff {q : } {x : } :
@[simp]
theorem irrational_int_sub_iff {m : } {x : } :
@[simp]
theorem irrational_nat_sub_iff {n : } {x : } :
@[simp]
theorem irrational_sub_rat_iff {q : } {x : } :
@[simp]
theorem irrational_sub_int_iff {m : } {x : } :
@[simp]
theorem irrational_sub_nat_iff {n : } {x : } :
@[simp]
theorem irrational_neg_iff {x : } :
@[simp]
theorem irrational_inv_iff {x : } :
@[simp]
theorem irrational_rat_mul_iff {q : } {x : } :
@[simp]
theorem irrational_mul_rat_iff {q : } {x : } :
@[simp]
theorem irrational_int_mul_iff {m : } {x : } :
@[simp]
theorem irrational_mul_int_iff {m : } {x : } :
@[simp]
theorem irrational_nat_mul_iff {n : } {x : } :
@[simp]
theorem irrational_mul_nat_iff {n : } {x : } :
@[simp]
theorem irrational_rat_div_iff {q : } {x : } :
@[simp]
theorem irrational_div_rat_iff {q : } {x : } :
@[simp]
theorem irrational_int_div_iff {m : } {x : } :
@[simp]
theorem irrational_div_int_iff {m : } {x : } :
@[simp]
theorem irrational_nat_div_iff {n : } {x : } :
@[simp]
theorem irrational_div_nat_iff {n : } {x : } :
theorem exists_irrational_btwn {x y : } (h : x < y) :
∃ (r : ), x < r r < y

There is an irrational number r between any two reals x < r < y.