coe_nsmul — Mathlib

English

The coercion commutes with natural scalar multiplication: (↑(n • x) : c.Quotient) = n • (x : c.Quotient).

Русский

Переобразование в фактор-множество и умножение на натуральное число согласованы: (↑(n • x)) = n • (↑x).

LaTeX

$$$$\left(↑(n \cdot x) : c.Quotient\right) = n \cdot (x : c.Quotient).$$$$

Lean4

@[simp, norm_cast]
theorem coe_nsmul (n : ℕ) (x : R) : (↑(n • x) : c.Quotient) = n • (x : c.Quotient) :=
  rfl

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