counit_C_mul_T — Mathlib

English

For any a in A and any integer n, the counit on the product C a · T n is equal to the counit on a; i.e., the counit is invariant under multiplication by monomials T n in the Laurent polynomial ring.

Русский

Для любого a ∈ A и любого целого числа n counit на произведении C(a) · T(n) равен counit на a; то есть counit инвариантен относитn к монономерам T n в кольце Лорана.

LaTeX

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

Lean4

@[simp]
theorem counit_C_mul_T (a : A) (n : ℤ) : Coalgebra.counit (R := R) (C a * T n) = Coalgebra.counit (R := R) a := by
  simp [← single_eq_C_mul_T]

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