coe_zsmul — Mathlib

English

Integer scalar multiplication commutes with the quotient map: for any n ∈ ℤ and x ∈ 𝕜, the class of n·x equals n times the class of x.

Русский

Целочисленное умножение совместимо с отражением в факторгруппе: для любого n ∈ ℤ и x ∈ 𝕜 класс n·x равен n-кратному классу x.

LaTeX

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

Lean4

theorem coe_zsmul {n : ℤ} {x : 𝕜} : (↑(n • x) : AddCircle p) = n • (x : AddCircle p) :=
  rfl

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