zsmul_eq_iff — Mathlib

English

If z ≠ 0, then z • ψ = z • θ iff there exists k forming ψ = θ + k · (2π / z).

Русский

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

LaTeX

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

Lean4

theorem zsmul_eq_iff {ψ θ : Angle} {z : ℤ} (hz : z ≠ 0) :
    z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + (k : ℕ) • (2 * π / z : ℝ) :=
  QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff hz

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