counit_pow

Mathlib.RingTheory.Bialgebra.Basic

URI: https://scilib.ai/kg/mathlib#Bialgebra.counit_pow

English

The counit preserves powers: counit(a^n) = counit(a)^n.

Русский

Коунил сохраняет степени: counit(a^n) = counit(a)^n.

LaTeX

$$$\forall a \in A,\ \forall n \in \mathbb{N},\ counit(a^n) = counit(a)^n$$$

Lean4

@[simp]
theorem counit_pow (a : A) (n : ℕ) : counit (R := R) (a ^ n) = counit a ^ n :=
  map_pow (counitAlgHom R A) a n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru