toCircle_add — Mathlib

English

The toCircle map is a homomorphism from angle addition to circle multiplication: toCircle(θ1 + θ2) = toCircle θ1 · toCircle θ2.

Русский

Отображение toCircle является гомоморфизмом от сложения углов к умножению на окружности: toCircle(θ1 + θ2) = toCircle θ1 · toCircle θ2.

LaTeX

$$$$ toCircle(\theta_1 + \theta_2) = toCircle(\theta_1) \cdot toCircle(\theta_2). $$$$

Lean4

@[simp]
theorem toCircle_add (θ₁ θ₂ : Angle) : toCircle (θ₁ + θ₂) = toCircle θ₁ * toCircle θ₂ :=
  by
  induction θ₁ using Real.Angle.induction_on
  induction θ₂ using Real.Angle.induction_on
  exact Circle.exp_add _ _

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