Extension of trigonometric functions to the complex plane

DefinitionCos (extension of trigonometric functions to the complex plane)#

The complex cosine function, defined via exp

Complex.cos (z : ℂ) : ℂ

Sources

• Mathlib documentation: Complex.cos
• Source of Complex.cos in Mathlib/Analysis/Complex/Trigonometric.lean
• Mathlib undergraduate list: Single Variable Complex Analysis › Complex-valued series › extension of trigonometric functions to the complex plane

MathlibComplex.cos

Uses 1 · Used by 24

Statement usesComplex exponential

Used byDe Moivre’s Formula · Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Leibniz’s Series for Pi · The Area of a Circle · Fourier Series · Stirling’s Formula · Cauchy integral formula · First Main Theorem of Value Distribution Theory · Phragmen-Lindelöf principle · Fourier transform as an integral · Riemann-Lebesgue lemma (Analysis) · Inverse trigonometric functions · Gaussian law · Mellin inversion theorem · Fourier theorem · Niven's theorem · Poisson’s formula · Fourier transforms on \(\mathcal{S}(\R^d)\) · Riemann-Lebesgue lemma (Measures and integral calculus) · Cos (power series expansion of elementary functions) · Cauchy formulas · Holomorphic stability under uniform convergence · Weierstrass trigonometric approximation theorem · Example, the Hilbert basis of trigonometric polynomials

DefinitionSin (extension of trigonometric functions to the complex plane)#

The complex sine function, defined via exp

Complex.sin (z : ℂ) : ℂ

Sources

• Mathlib documentation: Complex.sin
• Source of Complex.sin in Mathlib/Analysis/Complex/Trigonometric.lean
• Mathlib undergraduate list: Single Variable Complex Analysis › Complex-valued series › extension of trigonometric functions to the complex plane

MathlibComplex.sin

Uses 1 · Used by 3

Statement usesComplex exponential

Used byDe Moivre’s Formula · Trigonometric functions · Sin (power series expansion of elementary functions)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.