comul_pow

Mathlib.RingTheory.Bialgebra.Basic

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

English

The comultiplication preserves powers: comul(a^n) = comul(a)^n.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comul_pow (a : A) (n : ℕ) : comul (R := R) (a ^ n) = comul a ^ n :=
  map_pow (comulAlgHom R A) a n

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

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

Разделы

Аффилиация

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