Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.1
theorem Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.1 :
∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, defined in the `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.1` namespace, states that for any sort `α` and any two elements `a` and `b` of this sort, the statement "a equals b" is logically equivalent to the statement "b equals a". This theorem captures the symmetric property of equality in mathematics, which holds that if a equals b then b equals a, for all types.
More concisely: The theorem asserts that for all types `α` and elements `a`, `b` of type `α`, the equality `a = b` is logically equivalent to `b = a`.
|
Complex.cos_eq_one_iff
theorem Complex.cos_eq_one_iff : ∀ {x : ℂ}, x.cos = 1 ↔ ∃ k, ↑k * (2 * ↑Real.pi) = x
This theorem states that for all complex numbers 'x', the cosine of 'x' equals to one if and only if there exists an integer 'k' such that 'x' is equal to 'k' times '2π'. In other words, the cosine of a complex number equals to one precisely when that number is an integer multiple of '2π'. This theorem forms a connection between the cosine function and the multiples of '2π' in the complex number system.
More concisely: The complex number x has cosine equal to 1 if and only if x = k * 2π for some integer k.
|
Complex.tan_eq_zero_iff
theorem Complex.tan_eq_zero_iff : ∀ {θ : ℂ}, θ.tan = 0 ↔ ∃ k, ↑k * ↑Real.pi / 2 = θ
The theorem `Complex.tan_eq_zero_iff` states that the tangent of a complex number is equal to zero if and only if this number is equal to `k * π / 2` for some integer `k`. This theorem includes the consideration that zero is used as the "junk value" for division by zero. This theorem has a related theorem `Complex.tan_eq_zero_iff'`.
More concisely: The complex number `z` has tangent equal to zero if and only if `z` is equal to `k * (π/2)` for some integer `k`, where tangent is defined as the complex number quotient of the imaginary unit `i` and the complex number `1 + z * z`.
|
Complex.tan_eq_zero_iff'
theorem Complex.tan_eq_zero_iff' : ∀ {θ : ℂ}, θ.cos ≠ 0 → (θ.tan = 0 ↔ ∃ k, ↑k * ↑Real.pi = θ)
This theorem states that for any complex number θ, if the cosine of θ is not equal to zero (which ensures that the tangent of θ is well-defined), then the tangent of θ equals zero if and only if θ equals `k * π` for some integer `k`. In other words, the tangent of a complex number is zero exactly when that number is an integer multiple of π, provided that its cosine is nonzero. This theorem is related to, but slightly different from, the theorem `Complex.tan_eq_zero_iff`, which includes cases where θ yields "junk values".
More concisely: For complex numbers θ with non-zero cosine, the tangent of θ equals zero if and only if θ is an integer multiple of π.
|
Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.4
theorem Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.4 :
∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, (a = b - c) = (c + a = b)
This theorem states that for any type `G` that has an additive commutative group structure, given any three elements `a`, `b`, and `c` of `G`, the equation `a = b - c` is equivalent to the equation `c + a = b`. In other words, subtracting `c` from `b` to get `a` is the same as adding `c` to `a` to get `b`.
More concisely: For any additive commutative group `G`, the elements `a`, `b`, and `c` in `G` satisfy `a = b - c` if and only if `c + a = b`.
|
Complex.tan_add
theorem Complex.tan_add :
∀ {x y : ℂ},
(((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨
(∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑Real.pi / 2) →
(x + y).tan = (x.tan + y.tan) / (1 - x.tan * y.tan)
The theorem `Complex.tan_add` states that for any two complex numbers `x` and `y`, the tangent of the sum of `x` and `y` is equal to the sum of the tangents of `x` and `y` divided by `1` minus the product of the tangents of `x` and `y`, provided that neither `x` nor `y` is an odd multiple of half of π, or both `x` and `y` are odd multiples of half of π. In other words, if we denote by $k$ and $l$ any integers, then the condition can be written as: either for all $k$ and $l$, $x$ is not equal to $(2k+1)\pi/2$ and $y$ is not equal to $(2l+1)\pi/2$, or there exist such $k$ and $l$ that $x$ equals to $(2k+1)\pi/2$ and $y$ equals to $(2l+1)\pi/2$. The restriction is needed because the tangent function has poles at odd multiples of half of π.
More concisely: The theorem `Complex.tan_add` asserts that for complex numbers `x` and `y` not equal to odd multiples of half of π, their tangents add: `tan(x + y) = (tan x + tan y) / (1 - tan x * tan y)`.
|
Complex.cos_eq_zero_iff
theorem Complex.cos_eq_zero_iff : ∀ {θ : ℂ}, θ.cos = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑Real.pi / 2
This theorem states that for any complex number `θ`, the complex cosine function `Complex.cos θ` is equal to zero if and only if there exists an integer `k` such that `θ` equals `(2k + 1) * π / 2`, where `π` is the real number pi. In mathematical notation, this is saying: for all complex numbers `θ`, `cos(θ) = 0` if and only if `∃ k ∈ ℤ, θ = (2k + 1) * π / 2`.
More concisely: The complex cosine function equals zero if and only if the argument is a multiple of pi over 2, plus or minus an integer.
|
Real.mul_le_sin
theorem Real.mul_le_sin : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ x.sin
This theorem states that within the interval from 0 to π/2 (inclusive), the sine function has a linear lower bound. Specifically, for any real number `x` that lies within this range, the value of `sin(x)` is always greater than or equal to `2/π * x`. This inequality represents one part of Jordan's inequality; the other part is expressed in the theorem `Real.sin_lt`.
More concisely: For all real numbers `x` in the interval [0, π/2], the sine function satisfies the inequality sin(x) ≥ 2x/π.
|
Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.5
theorem Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex._auxLemma.5 :
∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, (a - b = c) = (a = c + b)
This theorem, from the Mathlib library in Lean, states that for any type `G` that is an additive group, and for any elements `a`, `b`, and `c` of that group, the statement "the difference of `a` and `b` equals `c`" is equivalent to the statement " `a` equals `c` added to `b`". This essentially derives from the properties of subtraction and addition in any group.
More concisely: For any additive group `G` and elements `a`, `b`, `c` in `G`, the equality `a - b = c` is equivalent to `a = c + b`.
|