ACounit_X — Mathlib

English

Let A, B be commutative semirings with an A-algebra structure, and let ACounit be the counit map on the multivariate polynomial algebra. For every b in B, the counit evaluates the indeterminate X_b to b.

Русский

Пусть A, B — коммутативные полукольца с A-алгебраической структурой, и существует каунит ACounit для многочленов с несколькими переменными. Для каждого b в B отображение каунит на X_b даёт b.

LaTeX

$$$ACounit_{A,B}(X_b) = b$$$

Lean4

@[simp]
theorem ACounit_X (b : B) : ACounit A B (X b) = b :=
  aeval_X _ b

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