id_apply_of_one_lt — Mathlib

English

For n ≠ 1, the n-th coefficient of the identity series id 𝕜 E is zero; i.e., (FormalMultilinearSeries.id 𝕜 E x) n = 0 for n > 1.

Русский

Для любых n, отличных от 1, n-й коэффициент id 𝕜 E равен нулю; то есть (FormalMultilinearSeries.id 𝕜 E x) n = 0 при n > 1.

LaTeX

$$$(id\\; 𝕜\\; E\\ x)_n = 0\\quad \\text{ for all } n > 1$.$$

Lean4

/-- For `n ≠ 1`, the `n`-th coefficient of `id 𝕜 E` is zero, by definition. -/
@[simp]
theorem id_apply_of_one_lt (x : E) {n : ℕ} (h : 1 < n) : (FormalMultilinearSeries.id 𝕜 E x) n = 0 := by
  match n with
  | 0 => contradiction
  | 1 => contradiction
  | n + 2 => rfl

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