abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi

English

If 2θ + 2ψ = π, then |cos θ| = |sin ψ|.

Русский

Если 2θ + 2ψ = π, то |cos θ| = |sin ψ|.

LaTeX

$$$(2:\mathbb{N})\cdot \theta + (2:\mathbb{N})\cdot \psi = \pi \Rightarrow |\cos \theta| = |\sin \psi|$$$

Lean4

theorem abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : Angle} (h : (2 : ℕ) • θ + (2 : ℕ) • ψ = π) :
    |cos θ| = |sin ψ| :=
  by
  rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h
  rcases h with (rfl | rfl) <;> simp [cos_pi_div_two_sub]

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