coeff_single — Mathlib

English

Let a ∈ G and b ∈ k. The coefficient function of the basis element single a b is the function that maps a to b and all other elements to 0; equivalently, coeff(single a b) = δ_{a,b}.

Русский

Пусть a ∈ G и b ∈ k. Коэффициентная функция базисного элемента single a b равна δ_{a,b}, то есть она принимает значение b на элементе a и 0 на прочих.

LaTeX

$$$\\operatorname{coeff}(\\mathrm{single}(a,b)) = \\delta_{a,b},$ где $\\delta_{a,b}(x) = \\begin{cases} b, & x=a, \\\\ 0, & x \\neq a. \\end{cases}$$$

Lean4

theorem coeff_single (a : G) (b : k) [DecidableEq G] : coeff (single a b) = Pi.single a b := by
  simp [coeff, Finsupp.single_eq_pi_single]

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