two_nsmul_eq_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem two_nsmul_eq_iff {ψ θ : Angle} : (2 : ℕ) • ψ = (2 : ℕ) • θ ↔ ψ = θ ∨ ψ = θ + ↑π := by
  simp_rw [← natCast_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]

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