sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi

English

sin(angle x y) = 0 iff angle x y = 0 or π.

Русский

sin(угол x y) = 0 тогда и только тогда, когда угол x y равен 0 или π.

LaTeX

$$sin(angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π$$

Lean4

/-- The sine of the angle between two vectors is 0 if and only if the angle is 0 or π. -/
theorem sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi : sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π := by
  rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_angle_eq_pi]

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