comul_natCast

Mathlib.RingTheory.Bialgebra.Basic

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

English

The comultiplication sends natural numbers embedded in A to the corresponding natural elements in A ⊗ A.

Русский

Коумуль отправляет натуральные числа, встроенные в A, к соответствующим элементам в A ⊗ A.

LaTeX

$$$\text{comul}(n) = n \quad (n \in \mathbb{N})$$$

Lean4

@[simp]
theorem comul_natCast (n : ℕ) : comul (R := R) (n : A) = n :=
  map_natCast (comulAlgHom R A) _

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

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

Разделы

Аффилиация

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