circleMap_zero_div — Mathlib

English

Division of two zero-centered circle maps corresponds to dividing radii and subtracting 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) \ / (circleMap 0 R2 θ2) = circleMap 0 (R1 / R2) (θ1 - θ2) $$$

Lean4

theorem circleMap_zero_div (R₁ R₂ θ₁ θ₂ : ℝ) :
    (circleMap 0 R₁ θ₁) / (circleMap 0 R₂ θ₂) = circleMap 0 (R₁ / R₂) (θ₁ - θ₂) :=
  by
  simp only [circleMap_zero, ofReal_div, ofReal_sub, sub_mul, Complex.exp_sub]
  ring

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