rename_comp_rename

Mathlib.Algebra.MvPolynomial.Rename

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

English

The same as above: (rename g) ∘ (rename f) = rename (g ∘ f).

Русский

То же самое: (rename g) ∘ (rename f) = rename (g ∘ f).

LaTeX

$$$\\text{rename } g \\; (\\text{rename } f\\, p) = \\text{rename } (g \\circ f)\\, p.$$$

Lean4

theorem rename_comp_rename (f : σ → τ) (g : τ → α) : (rename (R := R) g).comp (rename f) = rename (g ∘ f) :=
  AlgHom.ext fun p ↦ rename_rename f g p

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

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

Разделы

Аффилиация

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