ACounit_C

Mathlib.Algebra.MvPolynomial.Counit

URI: https://scilib.ai/kg/mathlib#MvPolynomial.ACounit_C

English

For any a in A, the counit map sends the constant polynomial C a to the image of a in B, i.e., algebraMap(a).

Русский

Для любого a ∈ A отображение каунит отправляет константный многочлен C a в изображение a в B, то есть algebraMap(a).

LaTeX

$$$ACounit_{A,B}(C a) = \ algebraMap_{A,B}(a)$$$

Lean4

theorem ACounit_C (a : A) : ACounit A B (C a) = algebraMap A B a :=
  aeval_C _ a

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

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

Разделы

Аффилиация

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