toCircle_neg — Mathlib

English

The image of the negated angle is the inverse on the circle: toCircle(−θ) = (toCircle(θ))^{-1}.

Русский

Образ отрицательного угла соответствует обратному на окружности: toCircle(−θ) = (toCircle(θ))^{-1}.

LaTeX

$$$$ toCircle(-\theta) = (toCircle(\theta))^{-1}. $$$$

Lean4

@[simp]
theorem toCircle_neg (θ : Angle) : toCircle (-θ) = (toCircle θ)⁻¹ :=
  by
  induction θ using Real.Angle.induction_on
  simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]

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