comap_id

Mathlib.Algebra.MvPolynomial.Comap

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

English

The comap with the identity algebra hom is the identity map on polynomials.

Русский

Comap по тождесвенной алгомомой — это тождественное отображение на многочленах.

LaTeX

$$$\\operatorname{comap}(\\mathrm{AlgHom.id\\,R\\, (MvPolynomial\\, σ\\, R)}) = \\mathrm{id}$$$

Lean4

theorem comap_id : comap (AlgHom.id R (MvPolynomial σ R)) = id :=
  by
  funext x
  exact comap_id_apply x

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

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

Разделы

Аффилиация

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