English
Let E be a normed space over 𝕜. The first coefficient of the identity formal multilinear series id 𝕜 E is the identity map on E; equivalently, for any x ∈ E and any v: Fin(1) → E, we have (id 𝕜 E x) 1 v = v 0.
Русский
Пусть E — нормированное пространство над 𝕜. Первая коэффициентная форма тождества формальной многочленовой серии id 𝕜 E является тождественным отображением на E; эквивалентно, для любого x ∈ E и любого v: Fin(1) → E выполняется (id 𝕜 E x) 1 v = v 0.
LaTeX
$$$( \\mathrm{FormalMultilinearSeries.id}\\; \\mathbb{K}\\; E\\ x)_1(v) = v_0,$ for all $x \\in E$ and $v: \\mathrm{Fin}(1) \\to E$.$$
Lean4
/-- The first coefficient of `id 𝕜 E` is the identity. -/
@[simp]
theorem id_apply_one (x : E) (v : Fin 1 → E) : (FormalMultilinearSeries.id 𝕜 E x) 1 v = v 0 :=
rfl
