coeff_single_apply — Mathlib

English

For all a, a' ∈ G and b ∈ k, the value of the coefficient at a' is b if a' = a and 0 otherwise.

Русский

Для любых a, a' ∈ G и b ∈ k коэффициент элемента single a b при a' равен b, если a' = a, и равен 0 иначе.

LaTeX

$$$\\operatorname{coeff}(\\mathrm{single}(a,b))(a') = \\begin{cases} b, & a'=a, \\\\ 0, & a' \\neq a. \\end{cases}$$$

Lean4

theorem coeff_single_apply {a a' : G} {b : k} [Decidable (a = a')] : coeff (single a b) a' = if a = a' then b else 0 :=
  by simp [coeff, Finsupp.single_apply]

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