coeff_index_single_X — Mathlib

English

For any s,t ∈ σ, the coefficient of X_s at index single t 1 is 1 if t = s, and 0 otherwise.

Русский

Пусть s,t ∈ σ. Коэффициент X_s на позиции single t 1 равен 1, если t = s, иначе 0.

LaTeX

$$$\operatorname{coeff}(\mathrm{single}(t,1)) (X_s) = \begin{cases} 1, & t = s \\ 0, & \text{otherwise} \end{cases}$$$

Lean4

theorem coeff_index_single_X [DecidableEq σ] (s t : σ) :
    coeff (single t 1) (X s : MvPowerSeries σ R) = if t = s then 1 else 0 := by
  simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

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