coe_nsmul — Mathlib

English

Natural scalar multiplication commutes with the quotient map into AddCircle p: for any n ∈ ℕ and x ∈ 𝕜, the class of n·x equals n times the class of x.

Русский

Естественная кратность действует совместно с фактором в AddCircle p: для любого n ∈ ℕ и x ∈ 𝕜 класс n·x равен n-кратному классу x.

LaTeX

$$$$ (\uparrow (n \cdot x) : AddCircle\ p) = n \cdot (x : AddCircle\ p) \quad\text{для всех } n \in \mathbb{N}, x \in 𝕜 $$$$

Lean4

theorem coe_nsmul {n : ℕ} {x : 𝕜} : (↑(n • x) : AddCircle p) = n • (x : AddCircle p) :=
  rfl

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