ofScalars_apply_zero — Mathlib

English

For each n, the nth coefficient applied to the zero input is given by a simple delta-like formula: ofScalars E c n (0-input) equals c(0) if n = 0 and equals 0 otherwise.

Русский

Для каждого n применение к нулевому аргументу даёт простую дельта-подобную формулу: (ofScalars E c n)(0) = c(0) если n=0 и равно 0 иначе.

LaTeX

$$$\forall n:\\mathbb{N},\; ofScalars E c n(0) = \begin{cases} c(0) & \text{if } n=0, \\ 0 & \text{if } n>0. \end{cases}$$$

Lean4

theorem ofScalars_apply_zero (n : ℕ) : ofScalars E c n (fun _ => 0) = Pi.single (M := fun _ => E) 0 (c 0 • 1) n :=
  by
  rw [ofScalars]
  cases n <;> simp

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