theorem
proved
tactic proof
dAlembert_double_angle
show as:
view Lean formalization →
formal statement (Lean)
67theorem dAlembert_double_angle (H : ℝ → ℝ)
68 (h_one : H 0 = 1)
69 (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
70 ∀ t, H (2 * t) = 2 * H t ^ 2 - 1 := by
proof body
Tactic-mode proof.
71 intro t
72 have h := h_dAlembert t t
73 have : t + t = 2 * t := by ring
74 rw [this] at h
75 have : t - t = 0 := by ring
76 rw [this, h_one] at h
77 nlinarith [sq (H t)]
78
79/-! ## §2 The Classification Prop (kept for backward compatibility) -/
80
81/-- The Aczél classification statement. Now a PROVED theorem, no longer a hypothesis. -/