circleMap_zero_mul — Mathlib

English

Multiplication of two zero-centered circle maps corresponds to multiplying radii and adding angles: (circleMap 0 R1 θ1)(circleMap 0 R2 θ2) = circleMap 0 (R1 R2) (θ1 + θ2).

Русский

Произведение двух отображений circleMap с нулевым центром соответствует умножению радиусов и сумме углов: (circleMap 0 R1 θ1)(circleMap 0 R2 θ2) = circleMap 0 (R1 R2) (θ1 + θ2).

LaTeX

$$$ (circleMap 0 R1 θ1) \cdot (circleMap 0 R2 θ2) = circleMap 0 (R1 R2) (θ1 + θ2) $$$

Lean4

theorem circleMap_zero_mul (R₁ R₂ θ₁ θ₂ : ℝ) :
    (circleMap 0 R₁ θ₁) * (circleMap 0 R₂ θ₂) = circleMap 0 (R₁ * R₂) (θ₁ + θ₂) :=
  by
  simp only [circleMap_zero, ofReal_mul, ofReal_add, add_mul, Complex.exp_add]
  ring

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