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 √(q : ℚ) is irrational if and only if ¬IsSquare q ∧ 0 ≤ q.

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

With the Decidable instances in this file, is possible to prove Irrational √n using decide, when n is a numeric literal or cast; but this only works if you unseal Nat.sqrt.iter in before the theorem where you use this proof.

def Irrational (x : ℝ) : Prop

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

Equations

• Irrational x = (x ∉ Set.range Rat.cast)

theorem irrational_iff_ne_rational (x : ℝ) : Irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b

theorem Transcendental.irrational {r : ℝ} (tr : Transcendental ℚ r) : Irrational 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) : Irrational 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)] (hxr : x ^ n = ↑m) (hv : multiplicity (↑p) m % n ≠ 0) : Irrational 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)] (Hpv : multiplicity (↑p) m % 2 = 1) : Irrational √↑m

@[simp]

theorem not_irrational_zero : ¬Irrational 0

@[simp]

theorem not_irrational_one : ¬Irrational 1

theorem irrational_sqrt_ratCast_iff_of_nonneg {q : ℚ} (hq : 0 ≤ q) : Irrational √↑q ↔ ¬IsSquare q

theorem irrational_sqrt_ratCast_iff {q : ℚ} : Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

theorem irrational_sqrt_intCast_iff_of_nonneg {z : ℤ} (hz : 0 ≤ z) : Irrational √↑z ↔ ¬IsSquare z

theorem irrational_sqrt_intCast_iff {z : ℤ} : Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z

theorem irrational_sqrt_natCast_iff {n : ℕ} : Irrational √↑n ↔ ¬IsSquare n

theorem irrational_sqrt_ofNat_iff {n : ℕ} [n.AtLeastTwo] : Irrational √(OfNat.ofNat n) ↔ ¬IsSquare (OfNat.ofNat n)

theorem Nat.Prime.irrational_sqrt {p : ℕ} (hp : Prime p) : Irrational √↑p

theorem irrational_sqrt_two : Irrational √2

Irrationality of the Square Root of 2

instance instDecidableIrrationalSqrtOfNatReal {n : ℕ} [n.AtLeastTwo] : Decidable (Irrational √(OfNat.ofNat n))

This can be used as

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

Equations

• instDecidableIrrationalSqrtOfNatReal = decidable_of_iff' (¬IsSquare (OfNat.ofNat n)) ⋯

instance instDecidableIrrationalSqrtCastReal (n : ℕ) : Decidable (Irrational √↑n)

Equations

• instDecidableIrrationalSqrtCastReal n = decidable_of_iff' (¬IsSquare n) ⋯

instance instDecidableIrrationalSqrtCastReal_1 (z : ℤ) : Decidable (Irrational √↑z)

Equations

• instDecidableIrrationalSqrtCastReal_1 z = decidable_of_iff' (¬IsSquare z ∧ 0 ≤ z) ⋯

instance instDecidableIrrationalSqrtCastReal_2 (q : ℚ) : Decidable (Irrational √↑q)

Equations

• instDecidableIrrationalSqrtCastReal_2 q = decidable_of_iff' (¬IsSquare 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 : ℚ) : 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 Irrational.ne_ofNat {x : ℝ} (h : Irrational x) (n : ℕ) [n.AtLeastTwo] : x ≠ OfNat.ofNat n

@[simp]

theorem Rat.not_irrational (q : ℚ) : ¬Irrational ↑q

@[simp]

theorem Int.not_irrational (m : ℤ) : ¬Irrational ↑m

@[simp]

theorem Nat.not_irrational (m : ℕ) : ¬Irrational ↑m

@[simp]

theorem not_irrational_ofNat (n : ℕ) [n.AtLeastTwo] : ¬Irrational (OfNat.ofNat n)

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_ratCast_add (q : ℚ) {x : ℝ} (h : Irrational (↑q + x)) : Irrational x

@[deprecated Irrational.of_ratCast_add (since := "2025-04-01")]

theorem Irrational.of_rat_add (q : ℚ) {x : ℝ} (h : Irrational (↑q + x)) : Irrational x

Alias of Irrational.of_ratCast_add.

theorem Irrational.ratCast_add (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (↑q + x)

@[deprecated Irrational.ratCast_add (since := "2025-04-01")]

theorem Irrational.rat_add (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (↑q + x)

Alias of Irrational.ratCast_add.

theorem Irrational.of_add_ratCast (q : ℚ) {x : ℝ} : Irrational (x + ↑q) → Irrational x

@[deprecated Irrational.of_add_ratCast (since := "2025-04-01")]

theorem Irrational.of_add_rat (q : ℚ) {x : ℝ} : Irrational (x + ↑q) → Irrational x

Alias of Irrational.of_add_ratCast.

theorem Irrational.add_ratCast (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (x + ↑q)

@[deprecated Irrational.add_ratCast (since := "2025-04-01")]

theorem Irrational.add_rat (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (x + ↑q)

Alias of Irrational.add_ratCast.

theorem Irrational.of_intCast_add {x : ℝ} (m : ℤ) (h : Irrational (↑m + x)) : Irrational x

@[deprecated Irrational.of_intCast_add (since := "2025-04-01")]

theorem Irrational.of_int_add {x : ℝ} (m : ℤ) (h : Irrational (↑m + x)) : Irrational x

Alias of Irrational.of_intCast_add.

theorem Irrational.of_add_intCast {x : ℝ} (m : ℤ) (h : Irrational (x + ↑m)) : Irrational x

@[deprecated Irrational.of_add_intCast (since := "2025-04-01")]

theorem Irrational.of_add_int {x : ℝ} (m : ℤ) (h : Irrational (x + ↑m)) : Irrational x

Alias of Irrational.of_add_intCast.

theorem Irrational.intCast_add {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (↑m + x)

@[deprecated Irrational.intCast_add (since := "2025-04-01")]

theorem Irrational.int_add {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (↑m + x)

Alias of Irrational.intCast_add.

theorem Irrational.add_intCast {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (x + ↑m)

@[deprecated Irrational.add_intCast (since := "2025-04-01")]

theorem Irrational.add_int {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (x + ↑m)

Alias of Irrational.add_intCast.

theorem Irrational.of_natCast_add {x : ℝ} (m : ℕ) (h : Irrational (↑m + x)) : Irrational x

@[deprecated Irrational.of_natCast_add (since := "2025-04-01")]

theorem Irrational.of_nat_add {x : ℝ} (m : ℕ) (h : Irrational (↑m + x)) : Irrational x

Alias of Irrational.of_natCast_add.

theorem Irrational.of_add_natCast {x : ℝ} (m : ℕ) (h : Irrational (x + ↑m)) : Irrational x

@[deprecated Irrational.of_add_natCast (since := "2025-04-01")]

theorem Irrational.of_add_nat {x : ℝ} (m : ℕ) (h : Irrational (x + ↑m)) : Irrational x

Alias of Irrational.of_add_natCast.

theorem Irrational.natCast_add {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (↑m + x)

@[deprecated Irrational.natCast_add (since := "2025-04-01")]

theorem Irrational.nat_add {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (↑m + x)

Alias of Irrational.natCast_add.

theorem Irrational.add_natCast {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (x + ↑m)

@[deprecated Irrational.add_natCast (since := "2025-04-01")]

theorem Irrational.add_nat {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (x + ↑m)

Alias of Irrational.add_natCast.

Negation

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

theorem Irrational.neg {x : ℝ} (h : Irrational x) : Irrational (-x)

Subtraction of rational/integer/natural numbers

theorem Irrational.sub_ratCast (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (x - ↑q)

@[deprecated Irrational.sub_ratCast (since := "2025-04-01")]

theorem Irrational.sub_rat (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (x - ↑q)

Alias of Irrational.sub_ratCast.

theorem Irrational.ratCast_sub (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (↑q - x)

@[deprecated Irrational.ratCast_sub (since := "2025-04-01")]

theorem Irrational.rat_sub (q : ℚ) {x : ℝ} (h : Irrational x) : Irrational (↑q - x)

Alias of Irrational.ratCast_sub.

theorem Irrational.of_sub_ratCast (q : ℚ) {x : ℝ} (h : Irrational (x - ↑q)) : Irrational x

@[deprecated Irrational.of_sub_ratCast (since := "2025-04-01")]

theorem Irrational.of_sub_rat (q : ℚ) {x : ℝ} (h : Irrational (x - ↑q)) : Irrational x

Alias of Irrational.of_sub_ratCast.

theorem Irrational.of_ratCast_sub (q : ℚ) {x : ℝ} (h : Irrational (↑q - x)) : Irrational x

@[deprecated Irrational.of_ratCast_sub (since := "2025-04-01")]

theorem Irrational.of_rat_sub (q : ℚ) {x : ℝ} (h : Irrational (↑q - x)) : Irrational x

Alias of Irrational.of_ratCast_sub.

theorem Irrational.sub_intCast {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (x - ↑m)

@[deprecated Irrational.sub_intCast (since := "2025-04-01")]

theorem Irrational.sub_int {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (x - ↑m)

Alias of Irrational.sub_intCast.

theorem Irrational.intCast_sub {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (↑m - x)

@[deprecated Irrational.intCast_sub (since := "2025-04-01")]

theorem Irrational.int_sub {x : ℝ} (h : Irrational x) (m : ℤ) : Irrational (↑m - x)

Alias of Irrational.intCast_sub.

theorem Irrational.of_sub_intCast {x : ℝ} (m : ℤ) (h : Irrational (x - ↑m)) : Irrational x

@[deprecated Irrational.of_sub_intCast (since := "2025-04-01")]

theorem Irrational.of_sub_int {x : ℝ} (m : ℤ) (h : Irrational (x - ↑m)) : Irrational x

Alias of Irrational.of_sub_intCast.

theorem Irrational.of_intCast_sub {x : ℝ} (m : ℤ) (h : Irrational (↑m - x)) : Irrational x

@[deprecated Irrational.of_intCast_sub (since := "2025-04-01")]

theorem Irrational.of_int_sub {x : ℝ} (m : ℤ) (h : Irrational (↑m - x)) : Irrational x

Alias of Irrational.of_intCast_sub.

theorem Irrational.sub_natCast {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (x - ↑m)

@[deprecated Irrational.sub_natCast (since := "2025-04-01")]

theorem Irrational.sub_nat {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (x - ↑m)

Alias of Irrational.sub_natCast.

theorem Irrational.natCast_sub {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (↑m - x)

@[deprecated Irrational.natCast_sub (since := "2025-04-01")]

theorem Irrational.nat_sub {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (↑m - x)

Alias of Irrational.natCast_sub.

theorem Irrational.of_sub_natCast {x : ℝ} (m : ℕ) (h : Irrational (x - ↑m)) : Irrational x

@[deprecated Irrational.of_sub_natCast (since := "2025-04-01")]

theorem Irrational.of_sub_nat {x : ℝ} (m : ℕ) (h : Irrational (x - ↑m)) : Irrational x

Alias of Irrational.of_sub_natCast.

theorem Irrational.of_natCast_sub {x : ℝ} (m : ℕ) (h : Irrational (↑m - x)) : Irrational x

@[deprecated Irrational.of_natCast_sub (since := "2025-04-01")]

theorem Irrational.of_nat_sub {x : ℝ} (m : ℕ) (h : Irrational (↑m - x)) : Irrational x

Alias of Irrational.of_natCast_sub.

Multiplication by rational numbers

theorem Irrational.mul_cases {x y : ℝ} : Irrational (x * y) → Irrational x ∨ Irrational y

theorem Irrational.of_mul_ratCast (q : ℚ) {x : ℝ} (h : Irrational (x * ↑q)) : Irrational x

@[deprecated Irrational.of_mul_ratCast (since := "2025-04-01")]

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

Alias of Irrational.of_mul_ratCast.

theorem Irrational.mul_ratCast {x : ℝ} (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x * ↑q)

@[deprecated Irrational.mul_ratCast (since := "2025-04-01")]

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

Alias of Irrational.mul_ratCast.

theorem Irrational.of_ratCast_mul (q : ℚ) {x : ℝ} : Irrational (↑q * x) → Irrational x

@[deprecated Irrational.of_ratCast_mul (since := "2025-04-01")]

theorem Irrational.of_rat_mul (q : ℚ) {x : ℝ} : Irrational (↑q * x) → Irrational x

Alias of Irrational.of_ratCast_mul.

theorem Irrational.ratCast_mul {x : ℝ} (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (↑q * x)

@[deprecated Irrational.ratCast_mul (since := "2025-04-01")]

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

Alias of Irrational.ratCast_mul.

theorem Irrational.of_mul_intCast {x : ℝ} (m : ℤ) (h : Irrational (x * ↑m)) : Irrational x

@[deprecated Irrational.of_mul_intCast (since := "2025-04-01")]

theorem Irrational.of_mul_int {x : ℝ} (m : ℤ) (h : Irrational (x * ↑m)) : Irrational x

Alias of Irrational.of_mul_intCast.

theorem Irrational.of_intCast_mul {x : ℝ} (m : ℤ) (h : Irrational (↑m * x)) : Irrational x

@[deprecated Irrational.of_intCast_mul (since := "2025-04-01")]

theorem Irrational.of_int_mul {x : ℝ} (m : ℤ) (h : Irrational (↑m * x)) : Irrational x

Alias of Irrational.of_intCast_mul.

theorem Irrational.mul_intCast {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x * ↑m)

@[deprecated Irrational.mul_intCast (since := "2025-04-01")]

theorem Irrational.mul_int {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x * ↑m)

Alias of Irrational.mul_intCast.

theorem Irrational.intCast_mul {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (↑m * x)

@[deprecated Irrational.intCast_mul (since := "2025-04-01")]

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

Alias of Irrational.intCast_mul.

theorem Irrational.of_mul_natCast {x : ℝ} (m : ℕ) (h : Irrational (x * ↑m)) : Irrational x

@[deprecated Irrational.of_mul_natCast (since := "2025-04-01")]

theorem Irrational.of_mul_nat {x : ℝ} (m : ℕ) (h : Irrational (x * ↑m)) : Irrational x

Alias of Irrational.of_mul_natCast.

theorem Irrational.of_natCast_mul {x : ℝ} (m : ℕ) (h : Irrational (↑m * x)) : Irrational x

@[deprecated Irrational.of_natCast_mul (since := "2025-04-01")]

theorem Irrational.of_nat_mul {x : ℝ} (m : ℕ) (h : Irrational (↑m * x)) : Irrational x

Alias of Irrational.of_natCast_mul.

theorem Irrational.mul_natCast {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x * ↑m)

@[deprecated Irrational.mul_natCast (since := "2025-04-01")]

theorem Irrational.mul_nat {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x * ↑m)

Alias of Irrational.mul_natCast.

theorem Irrational.natCast_mul {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (↑m * x)

@[deprecated Irrational.natCast_mul (since := "2025-04-01")]

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

Alias of Irrational.natCast_mul.

Inverse

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

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_ratCast_div (q : ℚ) {x : ℝ} (h : Irrational (↑q / x)) : Irrational x

@[deprecated Irrational.of_ratCast_div (since := "2025-04-01")]

theorem Irrational.of_rat_div (q : ℚ) {x : ℝ} (h : Irrational (↑q / x)) : Irrational x

Alias of Irrational.of_ratCast_div.

theorem Irrational.of_div_ratCast (q : ℚ) {x : ℝ} (h : Irrational (x / ↑q)) : Irrational x

@[deprecated Irrational.of_div_ratCast (since := "2025-04-01")]

theorem Irrational.of_div_rat (q : ℚ) {x : ℝ} (h : Irrational (x / ↑q)) : Irrational x

Alias of Irrational.of_div_ratCast.

theorem Irrational.ratCast_div {x : ℝ} (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (↑q / x)

@[deprecated Irrational.ratCast_div (since := "2025-04-01")]

theorem Irrational.rat_div {x : ℝ} (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (↑q / x)

Alias of Irrational.ratCast_div.

theorem Irrational.div_ratCast {x : ℝ} (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x / ↑q)

@[deprecated Irrational.div_ratCast (since := "2025-04-01")]

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

Alias of Irrational.div_ratCast.

theorem Irrational.of_intCast_div {x : ℝ} (m : ℤ) (h : Irrational (↑m / x)) : Irrational x

@[deprecated Irrational.of_intCast_div (since := "2025-04-01")]

theorem Irrational.of_int_div {x : ℝ} (m : ℤ) (h : Irrational (↑m / x)) : Irrational x

Alias of Irrational.of_intCast_div.

theorem Irrational.of_div_intCast {x : ℝ} (m : ℤ) (h : Irrational (x / ↑m)) : Irrational x

@[deprecated Irrational.of_div_intCast (since := "2025-04-01")]

theorem Irrational.of_div_int {x : ℝ} (m : ℤ) (h : Irrational (x / ↑m)) : Irrational x

Alias of Irrational.of_div_intCast.

theorem Irrational.intCast_div {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (↑m / x)

@[deprecated Irrational.intCast_div (since := "2025-04-01")]

theorem Irrational.int_div {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (↑m / x)

Alias of Irrational.intCast_div.

theorem Irrational.div_intCast {x : ℝ} (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x / ↑m)

@[deprecated Irrational.div_intCast (since := "2025-04-01")]

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

Alias of Irrational.div_intCast.

theorem Irrational.of_natCast_div {x : ℝ} (m : ℕ) (h : Irrational (↑m / x)) : Irrational x

@[deprecated Irrational.of_natCast_div (since := "2025-04-01")]

theorem Irrational.of_nat_div {x : ℝ} (m : ℕ) (h : Irrational (↑m / x)) : Irrational x

Alias of Irrational.of_natCast_div.

theorem Irrational.of_div_natCast {x : ℝ} (m : ℕ) (h : Irrational (x / ↑m)) : Irrational x

@[deprecated Irrational.of_div_natCast (since := "2025-04-01")]

theorem Irrational.of_div_nat {x : ℝ} (m : ℕ) (h : Irrational (x / ↑m)) : Irrational x

Alias of Irrational.of_div_natCast.

theorem Irrational.natCast_div {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (↑m / x)

@[deprecated Irrational.natCast_div (since := "2025-04-01")]

theorem Irrational.nat_div {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (↑m / x)

Alias of Irrational.natCast_div.

theorem Irrational.div_natCast {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x / ↑m)

@[deprecated Irrational.div_natCast (since := "2025-04-01")]

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

Alias of Irrational.div_natCast.

theorem Irrational.of_one_div {x : ℝ} (h : Irrational (1 / x)) : Irrational x

Natural and integer power

theorem Irrational.of_mul_self {x : ℝ} (h : Irrational (x * x)) : Irrational 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_natDegree_of_irrational_root (x : ℝ) (p : Polynomial ℤ) (hx : Irrational x) (p_nonzero : p ≠ 0) (x_is_root : (Polynomial.aeval x) p = 0) : 1 < p.natDegree

Simplification lemmas about operations

@[simp]

theorem irrational_ratCast_add_iff {q : ℚ} {x : ℝ} : Irrational (↑q + x) ↔ Irrational x

@[deprecated irrational_ratCast_add_iff (since := "2025-04-01")]

theorem irrational_rat_add_iff {q : ℚ} {x : ℝ} : Irrational (↑q + x) ↔ Irrational x

Alias of irrational_ratCast_add_iff.

@[simp]

theorem irrational_intCast_add_iff {m : ℤ} {x : ℝ} : Irrational (↑m + x) ↔ Irrational x

@[deprecated irrational_intCast_add_iff (since := "2025-04-01")]

theorem irrational_int_add_iff {m : ℤ} {x : ℝ} : Irrational (↑m + x) ↔ Irrational x

Alias of irrational_intCast_add_iff.

@[simp]

theorem irrational_natCast_add_iff {n : ℕ} {x : ℝ} : Irrational (↑n + x) ↔ Irrational x

@[deprecated irrational_natCast_add_iff (since := "2025-04-01")]

theorem irrational_nat_add_iff {n : ℕ} {x : ℝ} : Irrational (↑n + x) ↔ Irrational x

Alias of irrational_natCast_add_iff.

@[simp]

theorem irrational_add_ratCast_iff {q : ℚ} {x : ℝ} : Irrational (x + ↑q) ↔ Irrational x

@[deprecated irrational_add_ratCast_iff (since := "2025-04-01")]

theorem irrational_add_rat_iff {q : ℚ} {x : ℝ} : Irrational (x + ↑q) ↔ Irrational x

Alias of irrational_add_ratCast_iff.

@[simp]

theorem irrational_add_intCast_iff {m : ℤ} {x : ℝ} : Irrational (x + ↑m) ↔ Irrational x

@[deprecated irrational_add_intCast_iff (since := "2025-04-01")]

theorem irrational_add_int_iff {m : ℤ} {x : ℝ} : Irrational (x + ↑m) ↔ Irrational x

Alias of irrational_add_intCast_iff.

@[simp]

theorem irrational_add_natCast_iff {n : ℕ} {x : ℝ} : Irrational (x + ↑n) ↔ Irrational x

@[deprecated irrational_add_natCast_iff (since := "2025-04-01")]

theorem irrational_add_nat_iff {n : ℕ} {x : ℝ} : Irrational (x + ↑n) ↔ Irrational x

Alias of irrational_add_natCast_iff.

@[simp]

theorem irrational_ratCast_sub_iff {q : ℚ} {x : ℝ} : Irrational (↑q - x) ↔ Irrational x

@[deprecated irrational_ratCast_sub_iff (since := "2025-04-01")]

theorem irrational_rat_sub_iff {q : ℚ} {x : ℝ} : Irrational (↑q - x) ↔ Irrational x

Alias of irrational_ratCast_sub_iff.

@[simp]

theorem irrational_intCast_sub_iff {m : ℤ} {x : ℝ} : Irrational (↑m - x) ↔ Irrational x

@[deprecated irrational_intCast_sub_iff (since := "2025-04-01")]

theorem irrational_int_sub_iff {m : ℤ} {x : ℝ} : Irrational (↑m - x) ↔ Irrational x

Alias of irrational_intCast_sub_iff.

@[simp]

theorem irrational_natCast_sub_iff {n : ℕ} {x : ℝ} : Irrational (↑n - x) ↔ Irrational x

@[deprecated irrational_natCast_sub_iff (since := "2025-04-01")]

theorem irrational_nat_sub_iff {n : ℕ} {x : ℝ} : Irrational (↑n - x) ↔ Irrational x

Alias of irrational_natCast_sub_iff.

@[simp]

theorem irrational_sub_ratCast_iff {q : ℚ} {x : ℝ} : Irrational (x - ↑q) ↔ Irrational x

@[deprecated irrational_sub_ratCast_iff (since := "2025-04-01")]

theorem irrational_sub_rat_iff {q : ℚ} {x : ℝ} : Irrational (x - ↑q) ↔ Irrational x

Alias of irrational_sub_ratCast_iff.

@[simp]

theorem irrational_sub_intCast_iff {m : ℤ} {x : ℝ} : Irrational (x - ↑m) ↔ Irrational x

@[deprecated irrational_sub_intCast_iff (since := "2025-04-01")]

theorem irrational_sub_int_iff {m : ℤ} {x : ℝ} : Irrational (x - ↑m) ↔ Irrational x

Alias of irrational_sub_intCast_iff.

@[simp]

theorem irrational_sub_natCast_iff {n : ℕ} {x : ℝ} : Irrational (x - ↑n) ↔ Irrational x

@[deprecated irrational_sub_natCast_iff (since := "2025-04-01")]

theorem irrational_sub_nat_iff {n : ℕ} {x : ℝ} : Irrational (x - ↑n) ↔ Irrational x

Alias of irrational_sub_natCast_iff.

@[simp]

theorem irrational_neg_iff {x : ℝ} : Irrational (-x) ↔ Irrational x

@[simp]

theorem irrational_inv_iff {x : ℝ} : Irrational x⁻¹ ↔ Irrational x

@[simp]

theorem irrational_ratCast_mul_iff {q : ℚ} {x : ℝ} : Irrational (↑q * x) ↔ q ≠ 0 ∧ Irrational x

@[deprecated irrational_ratCast_mul_iff (since := "2025-04-01")]

theorem irrational_rat_mul_iff {q : ℚ} {x : ℝ} : Irrational (↑q * x) ↔ q ≠ 0 ∧ Irrational x

Alias of irrational_ratCast_mul_iff.

@[simp]

theorem irrational_mul_ratCast_iff {q : ℚ} {x : ℝ} : Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x

@[deprecated irrational_mul_ratCast_iff (since := "2025-04-01")]

theorem irrational_mul_rat_iff {q : ℚ} {x : ℝ} : Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x

Alias of irrational_mul_ratCast_iff.

@[simp]

theorem irrational_intCast_mul_iff {m : ℤ} {x : ℝ} : Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x

@[deprecated irrational_intCast_mul_iff (since := "2025-04-01")]

theorem irrational_int_mul_iff {m : ℤ} {x : ℝ} : Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x

Alias of irrational_intCast_mul_iff.

@[simp]

theorem irrational_mul_intCast_iff {m : ℤ} {x : ℝ} : Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x

@[deprecated irrational_mul_intCast_iff (since := "2025-04-01")]

theorem irrational_mul_int_iff {m : ℤ} {x : ℝ} : Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x

Alias of irrational_mul_intCast_iff.

@[simp]

theorem irrational_natCast_mul_iff {n : ℕ} {x : ℝ} : Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

@[deprecated irrational_natCast_mul_iff (since := "2025-04-01")]

theorem irrational_nat_mul_iff {n : ℕ} {x : ℝ} : Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

Alias of irrational_natCast_mul_iff.

@[simp]

theorem irrational_mul_natCast_iff {n : ℕ} {x : ℝ} : Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

@[deprecated irrational_mul_natCast_iff (since := "2025-04-01")]

theorem irrational_mul_nat_iff {n : ℕ} {x : ℝ} : Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

Alias of irrational_mul_natCast_iff.

@[simp]

theorem irrational_ratCast_div_iff {q : ℚ} {x : ℝ} : Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x

@[deprecated irrational_ratCast_div_iff (since := "2025-04-01")]

theorem irrational_rat_div_iff {q : ℚ} {x : ℝ} : Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x

Alias of irrational_ratCast_div_iff.

@[simp]

theorem irrational_div_ratCast_iff {q : ℚ} {x : ℝ} : Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x

@[deprecated irrational_div_ratCast_iff (since := "2025-04-01")]

theorem irrational_div_rat_iff {q : ℚ} {x : ℝ} : Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x

Alias of irrational_div_ratCast_iff.

@[simp]

theorem irrational_intCast_div_iff {m : ℤ} {x : ℝ} : Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x

@[deprecated irrational_intCast_div_iff (since := "2025-04-01")]

theorem irrational_int_div_iff {m : ℤ} {x : ℝ} : Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x

Alias of irrational_intCast_div_iff.

@[simp]

theorem irrational_div_intCast_iff {m : ℤ} {x : ℝ} : Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x

@[deprecated irrational_div_intCast_iff (since := "2025-04-01")]

theorem irrational_div_int_iff {m : ℤ} {x : ℝ} : Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x

Alias of irrational_div_intCast_iff.

@[simp]

theorem irrational_natCast_div_iff {n : ℕ} {x : ℝ} : Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x

@[deprecated irrational_natCast_div_iff (since := "2025-04-01")]

theorem irrational_nat_div_iff {n : ℕ} {x : ℝ} : Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x

Alias of irrational_natCast_div_iff.

@[simp]

theorem irrational_div_natCast_iff {n : ℕ} {x : ℝ} : Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x

@[deprecated irrational_div_natCast_iff (since := "2025-04-01")]

theorem irrational_div_nat_iff {n : ℕ} {x : ℝ} : Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x

Alias of irrational_div_natCast_iff.

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.