coe_smul — Mathlib

English

Scaling a cocycle by a scalar x in the base ring is compatible with its coercion to a cochain: ↑(x • z) = x • z.

Русский

Умножение кокцикла на скаляр в базовой кольце согласуется с приведением к коцепу.

LaTeX

$$(↑(x • z) : Cochain F G n) = x • (z : Cochain F G n)$$

Lean4

@[simp]
theorem coe_smul (z : Cocycle F G n) (x : R) : (↑(x • z) : Cochain F G n) = x • (z : Cochain F G n) :=
  rfl

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