Irrational.of_inv
theorem Irrational.of_inv : ∀ {x : ℝ}, Irrational x⁻¹ → Irrational x
The theorem `Irrational.of_inv` states that for any real number `x`, if its reciprocal `x⁻¹` (1/x) is irrational, then `x` itself is also irrational. In other words, the irrationality is preserved under the operation of taking the reciprocal.
More concisely: If the reciprocal of a real number is irrational, then the number itself is irrational.
|
Irrational.mul_rat
theorem Irrational.mul_rat : ∀ {x : ℝ}, Irrational x → ∀ {q : ℚ}, q ≠ 0 → Irrational (x * ↑q)
The theorem `Irrational.mul_rat` asserts that for any real number `x`, if `x` is irrational (meaning it cannot be expressed as a ratio of two integers), then for any rational number `q` that is not zero, the product of `x` and `q` is also irrational. This essentially means that multiplying an irrational number by a non-zero rational number will always result in an irrational number.
More concisely: If a real number is irrational, then its product with any non-zero rational number is also irrational.
|
irrational_nrt_of_notint_nrt
theorem irrational_nrt_of_notint_nrt : ∀ {x : ℝ} (n : ℕ) (m : ℤ), x ^ n = ↑m → (¬∃ y, x = ↑y) → 0 < n → Irrational x
This theorem states that if `x` raised to the power of `n` (where `n` is a positive natural number) equals to an integer `m`, and `x` is not the `n`-th power of any integer, then `x` is an irrational number. In mathematical terms, if $x^n = m$ for some natural number $n > 0$ and integer $m$, and there does not exist an integer `y` such that $x = y^n$, then `x` is irrational.
More concisely: If an integer `m` is the `n`-th power of a natural number `x` for some `n > 0`, and `x` is not the `n`-th power of any integer, then `x` is irrational.
|
irrational_rat_mul_iff
theorem irrational_rat_mul_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (↑q * x) ↔ q ≠ 0 ∧ Irrational x
This theorem states that a product of a rational number `q` and a real number `x` is irrational if and only if `q` is not equal to zero, and `x` is irrational. In other words, it asserts the equivalence between two conditions: (1) the multiplication of a rational number with a real number resulting in an irrational number, and (2) the rational number being non-zero and the real number being irrational.
More concisely: A rational number times a real number is irrational if and only if the rational number is non-zero and the real number is irrational.
|
Irrational.rat_add
theorem Irrational.rat_add : ∀ (q : ℚ) {x : ℝ}, Irrational x → Irrational (↑q + x)
The theorem `Irrational.rat_add` asserts that for any rational number `q` and any real number `x` that is irrational, the sum of `q` and `x` (denoted `↑q + x` in Lean 4, where `↑q` is the real number corresponding to `q`) is also irrational. In other words, adding a rational number to an irrational number results in another irrational number.
More concisely: The sum of a rational number and an irrational number is irrational.
|
Irrational.div_cases
theorem Irrational.div_cases : ∀ {x y : ℝ}, Irrational (x / y) → Irrational x ∨ Irrational y
The theorem `Irrational.div_cases` states that for all real numbers `x` and `y`, if the quotient of `x` divided by `y` is an irrational number, then either `x` or `y` must be an irrational number. In other words, it is impossible to divide two rational numbers and get an irrational number as a result.
More concisely: If the quotient of real numbers `x` and `y` is an irrational number, then at least one of `x` and `y` is irrational.
|
Rat.not_irrational
theorem Rat.not_irrational : ∀ (q : ℚ), ¬Irrational ↑q
The theorem `Rat.not_irrational` states that for all rational numbers `q`, it is not the case that `q` is irrational. In other words, there are no rational numbers that are also irrational. This aligns with the mathematical definition where a number cannot be both rational and irrational at the same time.
More concisely: Every rational number is non-irrational. (Equivalently, there are no rational irrational numbers.)
|
Irrational.inv
theorem Irrational.inv : ∀ {x : ℝ}, Irrational x → Irrational x⁻¹
The theorem `Irrational.inv` states that for any real number `x`, if `x` is irrational, then its multiplicative inverse (or reciprocal) `x⁻¹` is also irrational. In other words, the irrationality is preserved under the operation of taking reciprocals.
More concisely: If a real number is irrational, then its multiplicative inverse is also irrational.
|
irrational_mul_rat_iff
theorem irrational_mul_rat_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
The theorem `irrational_mul_rat_iff` states that for any real number `x` and any rational number `q`, `x` multiplied by `q` is an irrational number if and only if `q` is not zero and `x` is an irrational number. In other words, the product of a non-zero rational number and an irrational number is itself an irrational number.
More concisely: For any irrational real number x and non-zero rational number q, the product x * q is an irrational number.
|
Transcendental.irrational
theorem Transcendental.irrational : ∀ {r : ℝ}, Transcendental ℚ r → Irrational r
This theorem states that if a real number is transcendental over the rational numbers, then that number is irrational. In other words, any real number that cannot be expressed as a root of a non-zero polynomial equation with coefficients in the rational numbers (which defines a transcendental number) is not equal to any rational number and hence, is irrational.
More concisely: A transcendental real number is irrational.
|
irrational_nrt_of_n_not_dvd_multiplicity
theorem irrational_nrt_of_n_not_dvd_multiplicity :
∀ {x : ℝ} (n : ℕ) {m : ℤ} (hm : m ≠ 0) (p : ℕ) [hp : Fact p.Prime],
x ^ n = ↑m → (multiplicity (↑p) m).get ⋯ % n ≠ 0 → Irrational x
This theorem states that for any real number `x`, natural number `n`, integer `m`, and natural number `p` where `p` is a prime number, if `x` to the power `n` equals `m` (which is not zero), and `n` does not divide the highest power of `p` that still divides `m` (in other words, the remainder when the multiplicity of `p` in `m` is divided by `n` is not zero), then `x` is an irrational number. This means that `x` cannot be expressed as a fraction of two integers.
More concisely: If real numbers `x`, natural number `n`, integer `m`, and prime number `p` satisfy `x^n = m` and the highest power of `p` that divides `m` has a non-zero remainder when divided by `n`, then `x` is irrational.
|
irrational_sqrt_two
theorem irrational_sqrt_two : Irrational √2
This is the theorem of the "Irrationality of the Square Root of 2". It states that the square root of 2 is an irrational number. In other words, the square root of 2 is not equal to any rational number, where a rational number is a number that can be expressed as the quotient of two integers.
More concisely: The square root of 2 is not a rational number.
|
Mathlib.Data.Real.Irrational._auxLemma.22
theorem Mathlib.Data.Real.Irrational._auxLemma.22 : ∀ {x : ℝ}, Irrational x⁻¹ = Irrational x
The theorem `Mathlib.Data.Real.Irrational._auxLemma.22` states that for all real numbers `x`, `x` is irrational if and only if its reciprocal `1/x` is irrational. In other words, a real number and its reciprocal share the same irrationality status. If a real number is irrational, so is its reciprocal and vice versa.
More concisely: For all real numbers x, x is irrational if and only if 1/x is irrational.
|
Irrational.ne_int
theorem Irrational.ne_int : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), x ≠ ↑m
This theorem states that for any real number `x`, if `x` is irrational (meaning it cannot be expressed as a ratio of two integers), then `x` is not equal to any integer `m`. In other words, an irrational real number cannot be an integer.
More concisely: An irrational real number is not equal to any integer.
|
Irrational.of_rat_add
theorem Irrational.of_rat_add : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q + x) → Irrational x
The theorem `Irrational.of_rat_add` states that for every rational number `q` and for any real number `x`, if the sum of `q` (casted to a real number) and `x` is irrational, then `x` is also irrational. In other words, if the sum of a rational and a real number is not equal to any rational number, then that real number itself must be irrational.
More concisely: If the sum of a rational number and a real number is irrational, then the real number is irrational.
|
Irrational.of_mul_rat
theorem Irrational.of_mul_rat : ∀ (q : ℚ) {x : ℝ}, Irrational (x * ↑q) → Irrational x
The theorem `Irrational.of_mul_rat` states that for every rational number `q` and for every real number `x`, if the product of `x` and `q` is an irrational number, then `x` itself is an irrational number. In other words, if multiplying `x` by the rational number `q` produces an irrational number, then `x` must have been irrational to begin with.
More concisely: If the product of a rational number and a real number is an irrational number, then the real number is irrational.
|
Irrational.int_add
theorem Irrational.int_add : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), Irrational (↑m + x)
The theorem `Irrational.int_add` states that for every real number `x`, if `x` is an irrational number, then for every integer `m`, the sum of the integer `m` and `x` is also an irrational number. In other words, the sum of an irrational number and any integer is still irrational.
More concisely: If `x` is an irrational real number, then `m + x` is also an irrational real number for every integer `m`.
|
Irrational.of_int_add
theorem Irrational.of_int_add : ∀ {x : ℝ} (m : ℤ), Irrational (↑m + x) → Irrational x
The theorem `Irrational.of_int_add` states that for all real numbers `x` and integers `m`, if the sum of `m` and `x` (where `m` is cast to a real number) is irrational, then `x` is also irrational. In other words, adding an integer to an irrational number results in another irrational number.
More concisely: If the sum of an irrational real number and an integer is irrational, then the original irrational number is also irrational.
|
Irrational.mul_cases
theorem Irrational.mul_cases : ∀ {x y : ℝ}, Irrational (x * y) → Irrational x ∨ Irrational y
The theorem `Irrational.mul_cases` states that for all real numbers `x` and `y`, if the product of `x` and `y` is an irrational number, then at least one of `x` or `y` must be irrational. In other words, it is not possible to obtain an irrational number by multiplying two rational numbers.
More concisely: If the product of two real numbers is irrational, then at least one of them is irrational.
|
Irrational.of_rat_mul
theorem Irrational.of_rat_mul : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q * x) → Irrational x
This theorem states that for any rational number `q` and any real number `x`, if the product of the rational `q` and the real `x` (denoted by `↑q * x`) is an irrational number, then `x` must also be an irrational number. In other words, it establishes that the property of being irrational is preserved under multiplication by a rational number.
More concisely: If a rational number times a real number results in an irrational number, then the real number is irrational.
|
Irrational.add_cases
theorem Irrational.add_cases : ∀ {x y : ℝ}, Irrational (x + y) → Irrational x ∨ Irrational y
The theorem `Irrational.add_cases` asserts that for any two real numbers `x` and `y`, if the sum of `x` and `y` is an irrational number (a number that can't be expressed as a ratio of two integers), then at least one of `x` and `y` must be an irrational number. This is an important property of irrational numbers related to their operation under addition.
More concisely: If the sum of real numbers x and y is an irrational number, then at least one of x and y is irrational.
|
Irrational.of_neg
theorem Irrational.of_neg : ∀ {x : ℝ}, Irrational (-x) → Irrational x
This theorem states that for any real number 'x', if the negation of 'x' (-x) is irrational (meaning that it cannot be expressed as a ratio of two integers), then 'x' itself is also irrational.
More concisely: If a real number x has an irrational negation, then x is irrational.
|
exists_irrational_btwn
theorem exists_irrational_btwn : ∀ {x y : ℝ}, x < y → ∃ r, Irrational r ∧ x < r ∧ r < y
This theorem states that for any two real numbers `x` and `y` such that `x` is less than `y`, there exists an irrational number `r` such that `r` is greater than `x` and less than `y`. In other words, between any two distinct real numbers, there is an irrational number.
More concisely: Between any two distinct real numbers, there exists an irrational number.
|
Irrational.int_mul
theorem Irrational.int_mul : ∀ {x : ℝ}, Irrational x → ∀ {m : ℤ}, m ≠ 0 → Irrational (↑m * x)
The theorem `Irrational.int_mul` states that for all real numbers `x`, if `x` is irrational (i.e., it cannot be expressed as a ratio of integers), then for all integers `m` not equal to zero, the product of `m` and `x` (with `m` cast to a real number) is also irrational. In mathematical terms, it asserts that the product of an irrational number and a nonzero integer is always an irrational number.
More concisely: If `x` is an irrational real number, then for all nonzero integers `m`, the product `m * x` is also an irrational real number.
|
Irrational.ne_nat
theorem Irrational.ne_nat : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), x ≠ ↑m
The theorem `Irrational.ne_nat` states that for all real numbers `x`, if `x` is irrational (i.e., it is not equal to any rational number), then `x` is not equal to the cast of any natural number `m`. In other words, an irrational real number cannot be equal to any natural number.
More concisely: An irrational real number does not equal any natural number.
|