nsmul_toReal_eq_mul — Mathlib

English

For natural n ≠ 0, (n • θ).toReal = n * θ.toReal iff θ.toReal ∈ (-π/n, π/n] (i.e., in Ioc(-π/n, π/n)).

Русский

Пусть натуральное n ≠ 0. Тогда (n • θ).toReal = n • θ.toReal эквивалентно $θ^{toReal}$ ∈ Ioc(-π/n, π/n).

LaTeX

$$$\\\\forall {n : \\mathbb{N}}, n \\\\neq 0 \\\\to \\\\forall {\\\\theta : Real.Angle}, \\\\Big( (n \\\\cdot \\\\theta).toReal = n * \\\\theta.toReal \\\\Big) \\\\iff \\\\theta.toReal ∈ \\\\mathrm{Ioc}(-\\\\pi / n) (\\\\pi / n)$$$

Lean4

theorem nsmul_toReal_eq_mul {n : ℕ} (h : n ≠ 0) {θ : Angle} :
    (n • θ).toReal = n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / n) (π / n) :=
  by
  nth_rw 1 [← coe_toReal θ]
  have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h
  rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h', le_div_iff₀' h']

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