id

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.id

English

There is a polynomial law id: M →ₚₗ[R] M that acts as the identity on M.

Русский

Существует полиномальное правило id: M →ₚₗ[R] M, действующее как тождественное отображение на M.

LaTeX

$$$\text{ id } : M \to_p_l[R] M$ with $\mathrm{toFun}'_S(x)=x$ for all S.$$

Lean4

/-- The identity as a polynomial law -/
def id : M →ₚₗ[R] M where toFun' S _ _ := _root_.id

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

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

Разделы

Аффилиация

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