rename_id_apply

Mathlib.Algebra.MvPolynomial.Rename

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

English

Applying the renaming map with the identity leaves a polynomial unchanged: rename id p = p.

Русский

Применение переименования по тождественному отображению оставляет полином без изменений: rename id p = p.

LaTeX

$$$\\text{rename id } p = p.$$$

Lean4

theorem rename_id_apply (p : MvPolynomial σ R) : rename id p = p := by simp

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

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

Разделы

Аффилиация

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