ofHamming_smul — Mathlib

English

The inverse encoding respects scalar multiplication: ofHamming(r • x) = r • ofHamming x.

Русский

Обратное кодирование сохраняет скалярное умножение: ofHamming(r • x) = r • ofHamming x.

LaTeX

$$$\\operatorname{ofHamming}(r \\cdot x) = r \\cdot \\operatorname{ofHamming}(x)$$$

Lean4

@[simp]
theorem ofHamming_smul [∀ i, SMul α (β i)] {r : α} {x : Hamming β} : ofHamming (r • x) = r • ofHamming x :=
  rfl

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