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.

source

def irrational :

ℝ → Prop

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

Equations

irrational x = (x ∉ set.range coe)

Irrationality of roots of integer and rational numbers

source

theorem irrational_nrt_of_notint_nrt {x : ℝ} (n : ℕ) (m : ℤ) :

x ^ n = ↑m → (¬∃ (y : ℤ), x = ↑y) → 0 < n → irrational x

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

source

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 ≠ 0 → irrational x

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

source

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

(multiplicity ↑p m).get _ % 2 = 1 → irrational (real.sqrt ↑m)

source

theorem nat.prime.irrational_sqrt {p : ℕ} :

nat.prime p → irrational (real.sqrt ↑p)

source

theorem irrational_sqrt_two :

irrational (real.sqrt 2)

source

theorem irrational_sqrt_rat_iff (q : ℚ) :

irrational (real.sqrt ↑q) ↔ rat.sqrt q * rat.sqrt q ≠ q ∧ 0 ≤ q

source

@[instance]

def irrational.decidable (q : ℚ) :

decidable (irrational (real.sqrt ↑q))

Equations

irrational.decidable q = decidable_of_iff' (rat.sqrt q * rat.sqrt q ≠ q ∧ 0 ≤ q) _

Adding/subtracting/multiplying by rational numbers

source

theorem rat.not_irrational (q : ℚ) :

¬irrational ↑q

source

theorem irrational.add_cases {x y : ℝ} :

irrational (x + y) → irrational x ∨ irrational y

source

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

irrational (↑q + x) → irrational x

source

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

irrational x → irrational (↑q + x)

source

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

irrational (x + ↑q) → irrational x

source

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

irrational x → irrational (x + ↑q)

source

theorem irrational.of_neg {x : ℝ} :

irrational (-x) → irrational x

source

theorem irrational.neg {x : ℝ} :

irrational x → irrational (-x)

source

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

irrational x → irrational (x - ↑q)

source

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

irrational x → irrational (↑q - x)

source

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

irrational (x - ↑q) → irrational x

source

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

irrational (↑q - x) → irrational x

source

theorem irrational.mul_cases {x y : ℝ} :

irrational (x * y) → irrational x ∨ irrational y

source

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

irrational (x * ↑q) → irrational x

source

theorem irrational.mul_rat {x : ℝ} (h : irrational x) {q : ℚ} :

q ≠ 0 → irrational (x * ↑q)

source

theorem irrational.of_rat_mul (q : ℚ) {x : ℝ} :

irrational (↑q * x) → irrational x

source

theorem irrational.rat_mul {x : ℝ} (h : irrational x) {q : ℚ} :

q ≠ 0 → irrational (↑q * x)

source

theorem irrational.of_mul_self {x : ℝ} :

irrational (x * x) → irrational x

source

theorem irrational.of_inv {x : ℝ} :

irrational x⁻¹ → irrational x

source

theorem irrational.inv {x : ℝ} :

irrational x → irrational x⁻¹

source

theorem irrational.div_cases {x y : ℝ} :

irrational (x / y) → irrational x ∨ irrational y

source

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

irrational (↑q / x) → irrational x

source

theorem irrational.of_one_div {x : ℝ} :

irrational (1 / x) → irrational x

source

theorem irrational.of_pow {x : ℝ} (n : ℕ) :

irrational (x ^ n) → irrational x

source

theorem irrational.of_fpow {x : ℝ} (m : ℤ) :

irrational (x ^ m) → irrational x

source

@[simp]

theorem irrational_rat_add_iff {q : ℚ} {x : ℝ} :

irrational (↑q + x) ↔ irrational x

source

@[simp]

theorem irrational_add_rat_iff {q : ℚ} {x : ℝ} :

irrational (x + ↑q) ↔ irrational x

source

@[simp]

theorem irrational_rat_sub_iff {q : ℚ} {x : ℝ} :

irrational (↑q - x) ↔ irrational x

source

@[simp]

theorem irrational_sub_rat_iff {q : ℚ} {x : ℝ} :

irrational (x - ↑q) ↔ irrational x

source

@[simp]

theorem irrational_neg_iff {x : ℝ} :

irrational (-x) ↔ irrational x

source

@[simp]

theorem irrational_inv_iff {x : ℝ} :

irrational x⁻¹ ↔ irrational x

mathlib documentation

data.real.irrational

Irrational real numbers

Irrationality of roots of integer and rational numbers

Adding/subtracting/multiplying by rational numbers

General documentation

Additional documentation

Library

mathlib documentation

data.​real.​irrational

Irrational real numbers

Irrationality of roots of integer and rational numbers

Adding/subtracting/multiplying by rational numbers

General documentation

Additional documentation

Library

data.real.irrational