pith. machine review for the scientific record. sign in
theorem proved term proof

euler_formula

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 203theorem euler_formula (θ : ℝ) :
 204    Complex.exp (I * θ) = Complex.cos θ + Complex.sin θ * I := by

proof body

Term-mode proof.

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

depends on (6)

Lean names referenced from this declaration's body.