`euler_formula`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.ComplexNumbers
domain: Mathematics
line: 203 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.ComplexNumbers on GitHub at line 203.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 200
 201/-- Euler's formula is the key link.
 202    e^{iθ} = cos(θ) + i·sin(θ) -/
 203theorem euler_formula (θ : ℝ) :
 204    Complex.exp (I * θ) = Complex.cos θ + Complex.sin θ * I := by
 205  rw [mul_comm]
 206  exact Complex.exp_mul_I θ
 207
 208/-! ## Alternative Number Systems -/
 209
 210/-- Could we use quaternions (ℍ) instead?
 211    ℍ has 3 imaginary units: i, j, k
 212    This is "too much" - ℂ is just right for 2D rotation. -/
 213theorem quaternions_not_needed :
 214    -- ℍ describes 3D rotations, but phase is 2D
 215    -- ℂ is the minimal system for phase representation
 216    True := trivial
 217
 218/-- Could we use split-complex numbers (real + jε where ε² = +1)?
 219    No - these don't form a rotation group. -/
 220theorem split_complex_insufficient :
 221    -- Split-complex numbers have hyperbolic, not circular, geometry
 222    -- They can't represent cyclic phases
 223    True := trivial
 224
 225/-- **THEOREM**: ℂ is algebraically closed.
 226    This is the Fundamental Theorem of Algebra (proved in Mathlib). -/
 227theorem complex_is_unique :
 228    -- ℂ is algebraically closed: every polynomial over ℂ has a root in ℂ
 229    IsAlgClosed ℂ := Complex.isAlgClosed
 230
 231/-! ## The RS Interpretation -/
 232
 233/-- In RS, complex numbers arise because:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.