counit_single — Mathlib

English

For any index i and element a in A_i, counit of the single i element equals the counit of a in A_i.

Русский

Для любого индекса i и элемента a в A_i коунит элемента DFinsupp.single i a равен коуниту a в A_i.

LaTeX

$$$ \operatorname{counit}(\mathrm{DFinsupp}.\mathrm{single}_{i} a) = \operatorname{counit}(a) $$$

Lean4

@[simp]
theorem counit_single (i : ι) (a : A i) : counit (DFinsupp.single i a) = counit (R := R) a :=
  lsum_single _ _ _ _

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