rename_id

Mathlib.Algebra.MvPolynomial.Rename

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

English

Renaming with the identity map is the identity map: rename id = id.

Русский

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

LaTeX

$$$\\text{rename id} = \\mathrm{id}_{\\mathrm{MvPolynomial}(\\sigma,R)}.$$$

Lean4

@[simp]
theorem rename_id : rename id = AlgHom.id R (MvPolynomial σ R) :=
  AlgHom.ext fun p ↦ eval₂_eta p

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

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

Разделы

Аффилиация

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