two_nsmul_eq_pi_iff — Mathlib

English

Let θ be an angle. Then (2)·θ = π if and only if θ = π/2 or θ = −π/2.

Русский

Пусть θ — угол. Тогда (2)·θ = π тогда эквивалентно θ = π/2 или θ = −π/2.

LaTeX

$$$2\,\theta = \pi \;\Longleftrightarrow\; \theta = \tfrac{\pi}{2} \;\lor\; \theta = -\tfrac{\pi}{2}$$$

Lean4

theorem two_nsmul_eq_pi_iff {θ : Angle} : (2 : ℕ) • θ = π ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ) :=
  by
  have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves]
  nth_rw 1 [h]
  rw [coe_nsmul, two_nsmul_eq_iff]
  apply iff_of_eq
  congr
  rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc, add_halves, ← two_mul,
    coe_two_pi]

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