coeff_apply — Mathlib

English

The coefficient map is piecewise: if i < natDegree f, use h.basis.repr; otherwise zero.

Русский

Коэффициентное отображение имеет разбиение: если i < natDegree f, то используется h.basis.repr, иначе нуль.

LaTeX

$$$ h.coeff z i = \\begin{cases} h.basis.repr z \\langle i, hi\\rangle, & i < \\operatorname{natDegree} f \\\\ 0, & \\text{ otherwise} \\end{cases} $$$

Lean4

theorem coeff_apply (z : S) (i : ℕ) : h.coeff z i = if hi : i < natDegree f then h.basis.repr z ⟨i, hi⟩ else 0 :=
  by
  split_ifs with hi
  · exact h.coeff_apply_lt z i hi
  · exact h.coeff_apply_le z i (le_of_not_gt hi)

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