order_one — Mathlib

English

The coefficient of 1 at index a is 1 if a=0, else 0; i.e., (1).coeff a = δ_{a,0}.

Русский

Коэффициент единицы в позиции a равен 1 если a=0, иначе 0.

LaTeX

$$$\mathrm{coeff}(1, a) = \begin{cases}1, & a=0\\0, & a\neq 0\end{cases}$$$

Lean4

@[simp]
theorem order_one [MulZeroOneClass R] : order (1 : HahnSeries Γ R) = 0 :=
  by
  cases subsingleton_or_nontrivial R
  · rw [Subsingleton.elim (1 : HahnSeries Γ R) 0, order_zero]
  · exact order_single one_ne_zero

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