counit_C — Mathlib

English

Let R be a commutative semiring and A a semiring with a coalgebra structure over R. For every a in A, the counit on the Laurent polynomial C a agrees with the counit on a; i.e., the evaluation at 1 behaves compatibly with passing to Laurent polynomials.

Русский

Пусть R — коммутативное полугрупповое кольцо, а A — полугруппа с коалгебраической структурой над R. Для каждого a ∈ A.counit на Laurent-полиноме C a совпадает с counit на a; то есть оценка в 1 сохраняется при переходе к полиномам Лорана.

LaTeX

$$$\operatorname{counit}_R( C(a) ) = \operatorname{counit}_R(a)$.$$

Lean4

@[simp]
theorem counit_C (a : A) : Coalgebra.counit (R := R) (C a) = Coalgebra.counit (R := R) a :=
  counit_single _ _

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