coe_nsmul — Mathlib

English

The underlying function of n • f is equal to applying n to the underlying function of f, i.e., the coe map commutes with nsmul.

Русский

Функциональное представление n • f равно применению n к базовой функции f; сопоставление приводимого вида согласуется с умножением на n.

LaTeX

$$$\forall n \in \mathbb{N}, \forall f:\iota \to_0 M,\ \text{coe}(n \cdot f) = n \cdot \text{coe}(f).$$$

Lean4

@[simp, norm_cast]
theorem coe_nsmul (n : ℕ) (f : ι →₀ M) : ⇑(n • f) = n • ⇑f :=
  rfl

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