smul_def — Mathlib

English

In the direct limit, multiplication is compatible with representatives: the product of the images of x and y is the image of the product.

Русский

В предельном лимите умножение совместимо с представителями: образ произведения равен образу произведения.

LaTeX

$$$ \forall i, x,y:\; \llbracket i,x \rrbracket \cdot \llbracket i,y \rrbracket = \llbracket i, x\,y \rrbracket $$$

Lean4

@[to_additive]
theorem smul_def (i x) (r : R) : r • ⟦⟨i, x⟩⟧ = (⟦⟨i, r • x⟩⟧ : DirectLimit G f) :=
  rfl

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