counitNat_surjective

Mathlib.Algebra.MvPolynomial.Counit

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

English

The counitNat map for any A is surjective; every element of A is the image of some polynomial under counitNat.

Русский

Отображение counitNat для любого A сюръективно; каждый элемент A является образом некоторого многочлена под counitNat.

LaTeX

$$$\text{Surjective}(\mathrm{counitNat}_A)$$$

Lean4

theorem counitNat_surjective : Surjective (counitNat A) :=
  ACounit_surjective ℕ A

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

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

Разделы

Аффилиация

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