Documentation

Mathlib.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 √(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 : ) :

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

Equations
Instances For
    theorem irrational_iff_ne_rational (x : ) :
    Irrational x ∀ (a b : ), x a / b

    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 % 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 % 2 = 1) :

    Irrationality of the Square Root of 2

    @[deprecated irrational_sqrt_ratCast_iff]

    This can be used as

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

    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] :
    @[simp]
    theorem Rat.not_irrational (q : ) :
    @[simp]
    theorem Int.not_irrational (m : ) :
    @[simp]
    theorem Nat.not_irrational (m : ) :
    @[simp]
    theorem not_irrational_ofNat (n : ) [n.AtLeastTwo] :

    Addition of rational/integer/natural numbers #

    theorem Irrational.add_cases {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) :
    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.neg {x : } (h : 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.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 #

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

    Natural and integer power #

    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_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_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.