mk_smul — Mathlib

English

The canonical representative respects scalar multiplication: mk(m · i) = m · mk(i) for i in NumDenSameDeg 𝒜 x and m in α.

Русский

Канонический представитель сохраняет скалярное умножение: mk(m · i) = m · mk(i) для i ∈ NumDenSameDeg 𝒜 x и m ∈ α.

LaTeX

$$$\mathrm{mk}\big(m\cdot i\big) = m\cdot\mathrm{mk}(i)$$$

Lean4

@[simp]
theorem mk_smul (i : NumDenSameDeg 𝒜 x) (m : α) : mk (m • i) = m • mk i :=
  rfl

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