nsmul_eq_iff — Mathlib

English

If n ≠ 0, then n • ψ = n • θ iff there exists k ∈ Fin n such that ψ = θ + k · (2π / n).

Русский

Если n ≠ 0, то n • ψ = n • θ тогда и только тогда, когда существует k ∈ Fin n такое, что ψ = θ + k · (2π / n).

LaTeX

$$$ n \cdot \psi = n \cdot \theta \\iff \\exists k : Fin n, \\psi = \theta + (k : \mathbb{N}) \cdot (2 \pi / n : \mathbb{R}). $$$

Lean4

theorem nsmul_eq_iff {ψ θ : Angle} {n : ℕ} (hz : n ≠ 0) :
    n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (2 * π / n : ℝ) :=
  QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff hz

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