sin_pi_mul_ne_zero — Mathlib

English

If x is not an integer, then sin(π x) ≠ 0.

Русский

Если x не целое, то sin(π x) ≠ 0.

LaTeX

$$$$\forall x \notin \mathbb{Z}, \; \sin(\pi x) \neq 0.$$$$

Lean4

/-- `sin π z` is non vanishing on the complement of the integers in `ℂ`. -/
theorem sin_pi_mul_ne_zero (hx : x ∈ ℂ_ℤ) : Complex.sin (π * x) ≠ 0 :=
  by
  apply Complex.sin_ne_zero_iff.2
  intro k
  nth_rw 2 [mul_comm]
  exact Injective.ne (mul_right_injective₀ (ofReal_ne_zero.mpr Real.pi_ne_zero)) (by aesop)

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