coe_units_smul — Mathlib

English

Multiplication by a units element x ∈ Rˣ respects the cocycle structure via the smul action on Cocycle F G n.

Русский

Умножение на элемент-единицу x ∈ Rˣ сохраняет структуру кокцикла через скалярное действие на Cocycle.

LaTeX

$$The action by units preserves cocycles: (x • z) ∈ Cocycle F G n whenever z ∈ Cocycle F G n and x ∈ Rˣ.$$

Lean4

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

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