sin_add — Mathlib

English

For all angles θ1, θ2, sin(θ1 + θ2) = sin θ1 cos θ2 + cos θ1 sin θ2.

Русский

Для любых углов θ1, θ2 верно sin(θ1 + θ2) = sin θ1 cos θ2 + cos θ1 sin θ2.

LaTeX

$$$\sin(\theta_1 + \theta_2) = \sin \theta_1 \cos \theta_2 + \cos \theta_1 \sin \theta_2$$$

Lean4

theorem sin_add (θ₁ θ₂ : Real.Angle) : sin (θ₁ + θ₂) = sin θ₁ * cos θ₂ + cos θ₁ * sin θ₂ :=
  by
  induction θ₁ using Real.Angle.induction_on
  induction θ₂ using Real.Angle.induction_on
  exact Real.sin_add _ _

Похожие утверждения