two_zsmul_eq_iff — Mathlib

English

For ψ, θ ∈ Angle, (2)•ψ = (2)•θ iff ψ = θ or ψ = θ + π.

Русский

Для ψ, θ ∈ угол, (2)•ψ = (2)•θ тогда и только тогда, когда ψ = θ или ψ = θ + π.

LaTeX

$$$ (2 : \mathbb{Z}) \cdot \psi = (2 : \mathbb{Z}) \cdot \theta \\iff \psi = \theta \;\lor\; \psi = \theta + \uparrow(\\pi). $$$

Lean4

theorem two_zsmul_eq_iff {ψ θ : Angle} : (2 : ℤ) • ψ = (2 : ℤ) • θ ↔ ψ = θ ∨ ψ = θ + ↑π :=
  by
  have : Int.natAbs 2 = 2 := rfl
  rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero, Fin.val_one, zero_smul, add_zero, one_smul,
    Int.cast_two, mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]

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