coe_zsmul — Mathlib

English

The coercion preserves integer scalar multiplication: (z • x) coerces to the quotient equals z • (x coerced).

Русский

Приведение сохраняет целочисленное умножение: (z • x) в кодек равняется z • (x в кодек).

LaTeX

$$$ (\\uparrow (z \\cdot x) : c.Quotient) = z \\cdot (x : c.Quotient)$$$

Lean4

@[simp, norm_cast]
theorem coe_zsmul (z : ℤ) (x : R) : (↑(z • x) : c.Quotient) = z • (x : c.Quotient) :=
  rfl

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