counitNat_X

Mathlib.Algebra.MvPolynomial.Counit

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

English

For any a in A, counitNat A (X a) = a.

Русский

Для любого a ∈ A, counitNat A (X a) = a.

LaTeX

$$$\mathrm{counitNat}_A(X a) = a\quad(a \in A)$$$

Lean4

@[simp]
theorem counitNat_X (a : A) : counitNat A (X a) = a :=
  ACounit_X _ _

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

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

Разделы

Аффилиация

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