mathlib3 documentation

data.real.irrational

Irrational real numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

irrational x = (x ∉ set.range coe)

Instances for irrational

irrational.decidable

theorem irrational_iff_ne_rational (x : ℝ) :

irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b

theorem transcendental.irrational {r : ℝ} (tr : transcendental ℚ 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 : (multiplicity ↑p 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 : (multiplicity ↑p m).get _ % 2 = 1) :

irrational (√ ↑m)

theorem nat.prime.irrational_sqrt {p : ℕ} (hp : nat.prime p) :

irrational (√ ↑p)

theorem irrational_sqrt_two :

irrational (√ 2)

Irrationality of the Square Root of 2

theorem irrational_sqrt_rat_iff (q : ℚ) :

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

@[protected, instance]

def irrational.decidable (q : ℚ) :

decidable (irrational (√ ↑q))

Equations

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

Dot-style operations on `irrational` #

Coercion of a rational/integer/natural number is not irrational #

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

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

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

theorem irrational.ne_nat {x : ℝ} (h : irrational 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 : ℚ) :

¬irrational ↑q

@[simp]

theorem int.not_irrational (m : ℤ) :

¬irrational ↑m

@[simp]

theorem nat.not_irrational (m : ℕ) :

¬irrational ↑m

Addition of rational/integer/natural numbers #

theorem irrational.add_cases {x y : ℝ} :

irrational (x + y) → irrational x ∨ irrational 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) :

irrational (↑q + x)

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

irrational (x + ↑q) → irrational x

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

irrational (x + ↑q)

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 : ℤ) :

irrational (↑m + x)

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

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 : ℕ) :

irrational (↑m + x)

theorem irrational.add_nat {x : ℝ} (h : irrational x) (m : ℕ) :

irrational (x + ↑m)

Negation #

theorem irrational.of_neg {x : ℝ} (h : irrational (-x)) :

@[protected]

theorem irrational.neg {x : ℝ} (h : irrational x) :

irrational (-x)

Subtraction of rational/integer/natural numbers #

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

irrational (x - ↑q)

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

irrational (↑q - 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 : ℤ) :

irrational (x - ↑m)

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

irrational (↑m - x)

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 : ℕ) :

irrational (x - ↑m)

theorem irrational.nat_sub {x : ℝ} (h : irrational x) (m : ℕ) :

irrational (↑m - x)

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) → irrational x ∨ irrational y

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

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

irrational (x * ↑q)

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

irrational (↑q * x) → irrational x

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

irrational (↑q * x)

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) :

irrational (x * ↑m)

theorem irrational.int_mul {x : ℝ} (h : irrational x) {m : ℤ} (hm : m ≠ 0) :

irrational (↑m * x)

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) :

irrational (x * ↑m)

theorem irrational.nat_mul {x : ℝ} (h : irrational x) {m : ℕ} (hm : m ≠ 0) :

irrational (↑m * x)

Inverse #

theorem irrational.of_inv {x : ℝ} (h : irrational x⁻¹) :

@[protected]

theorem irrational.inv {x : ℝ} (h : irrational x) :

irrational x⁻¹

Division #

theorem irrational.div_cases {x y : ℝ} (h : irrational (x / y)) :

irrational x ∨ irrational 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) :

irrational (↑q / x)

theorem irrational.div_rat {x : ℝ} (h : irrational x) {q : ℚ} (hq : q ≠ 0) :

irrational (x / ↑q)

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) :

irrational (↑m / x)

theorem irrational.div_int {x : ℝ} (h : irrational x) {m : ℤ} (hm : m ≠ 0) :

irrational (x / ↑m)

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) :

irrational (↑m / x)

theorem irrational.div_nat {x : ℝ} (h : irrational x) {m : ℕ} (hm : m ≠ 0) :

irrational (x / ↑m)

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) → irrational x

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

irrational (x ^ m) → irrational x

theorem one_lt_nat_degree_of_irrational_root (x : ℝ) (p : polynomial ℤ) (hx : irrational x) (p_nonzero : p ≠ 0) (x_is_root : ⇑(polynomial.aeval x) p = 0) :

1 < p.nat_degree

Simplification lemmas about operations #

@[simp]

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

irrational (↑q + x) ↔ irrational x

@[simp]

theorem irrational_int_add_iff {m : ℤ} {x : ℝ} :

irrational (↑m + x) ↔ irrational x

@[simp]

theorem irrational_nat_add_iff {n : ℕ} {x : ℝ} :

irrational (↑n + x) ↔ irrational x

@[simp]

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

irrational (x + ↑q) ↔ irrational x

@[simp]

theorem irrational_add_int_iff {m : ℤ} {x : ℝ} :

irrational (x + ↑m) ↔ irrational x

@[simp]

theorem irrational_add_nat_iff {n : ℕ} {x : ℝ} :

irrational (x + ↑n) ↔ irrational x

@[simp]

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

irrational (↑q - x) ↔ irrational x

@[simp]

theorem irrational_int_sub_iff {m : ℤ} {x : ℝ} :

irrational (↑m - x) ↔ irrational x

@[simp]

theorem irrational_nat_sub_iff {n : ℕ} {x : ℝ} :

irrational (↑n - x) ↔ irrational x

@[simp]

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

irrational (x - ↑q) ↔ irrational x

@[simp]

theorem irrational_sub_int_iff {m : ℤ} {x : ℝ} :

irrational (x - ↑m) ↔ irrational x

@[simp]

theorem irrational_sub_nat_iff {n : ℕ} {x : ℝ} :

irrational (x - ↑n) ↔ irrational x

@[simp]

theorem irrational_neg_iff {x : ℝ} :

irrational (-x) ↔ irrational x

@[simp]

theorem irrational_inv_iff {x : ℝ} :

irrational x⁻¹ ↔ irrational x

@[simp]

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

irrational (↑q * x) ↔ q ≠ 0 ∧ irrational x

@[simp]

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

irrational (x * ↑q) ↔ q ≠ 0 ∧ irrational x

@[simp]

theorem irrational_int_mul_iff {m : ℤ} {x : ℝ} :

irrational (↑m * x) ↔ m ≠ 0 ∧ irrational x

@[simp]

theorem irrational_mul_int_iff {m : ℤ} {x : ℝ} :

irrational (x * ↑m) ↔ m ≠ 0 ∧ irrational x

@[simp]

theorem irrational_nat_mul_iff {n : ℕ} {x : ℝ} :

irrational (↑n * x) ↔ n ≠ 0 ∧ irrational x

@[simp]

theorem irrational_mul_nat_iff {n : ℕ} {x : ℝ} :

irrational (x * ↑n) ↔ n ≠ 0 ∧ irrational x

@[simp]

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

irrational (↑q / x) ↔ q ≠ 0 ∧ irrational x

@[simp]

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

irrational (x / ↑q) ↔ q ≠ 0 ∧ irrational x

@[simp]

theorem irrational_int_div_iff {m : ℤ} {x : ℝ} :

irrational (↑m / x) ↔ m ≠ 0 ∧ irrational x

@[simp]

theorem irrational_div_int_iff {m : ℤ} {x : ℝ} :

irrational (x / ↑m) ↔ m ≠ 0 ∧ irrational x

@[simp]

theorem irrational_nat_div_iff {n : ℕ} {x : ℝ} :

irrational (↑n / x) ↔ n ≠ 0 ∧ irrational x

@[simp]

theorem irrational_div_nat_iff {n : ℕ} {x : ℝ} :

irrational (x / ↑n) ↔ n ≠ 0 ∧ irrational x

theorem exists_irrational_btwn {x y : ℝ} (h : x < y) :

∃ (r : ℝ), irrational r ∧ x < r ∧ r < y

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