counit_natCast

Mathlib.RingTheory.Bialgebra.Basic

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

English

The counit sends natural numbers embedded in A to themselves.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem counit_natCast (n : ℕ) : counit (R := R) (n : A) = n :=
  map_natCast (counitAlgHom R A) _

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

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

Разделы

Аффилиация

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