theorem proved term proof

`euler_from_8tick`

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

formal statement (Lean)

 156theorem euler_from_8tick :
 157    ∀ θ : ℝ, cexp (I * θ) = Complex.cos θ + I * Complex.sin θ := by

proof body

Term-mode proof.

 158  intro θ
 159  rw [Complex.exp_mul_I]
 160  ring
 161
 162/-- e^{iπ} + 1 = 0 (Euler's identity)
 163
 164    Often called "the most beautiful equation."
 165    In RS, it says: 4 ticks around the circle returns to -1. -/

depends on (2)

Lean names referenced from this declaration's body.

identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use