natCast_mul_eq_nsmul — Mathlib

English

Let x ∈ ℝ and n ∈ ℕ. The angle corresponding to n x equals n times the angle corresponding to x.

Русский

Пусть x ∈ ℝ и n ∈ ℕ. Угол, соответствующий n x, равен n-кратному углу, соответствующему x.

LaTeX

$$$ \\uparrow\big((n : \mathbb{R}) \, x\big) = n \cdot (\\uparrow x : \\mathrm{Angle}) $$$

Lean4

@[simp, norm_cast]
theorem natCast_mul_eq_nsmul (x : ℝ) (n : ℕ) : ↑((n : ℝ) * x) = n • (↑x : Angle) := by
  simpa only [nsmul_eq_mul] using coeHom.map_nsmul x n

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