of_symm_X_smul

Mathlib.Algebra.Polynomial.Module.AEval

URI: https://scilib.ai/kg/mathlib#Module.AEval'.of_symm_X_smul

English

Symm X-scalar action commutes with the restriction to submodules in AEval.

Русский

Действие X через симметрическое умножение согласуется с ограничением до подмодуля AEval.

LaTeX

$$$(X)\text{-smul}$ commutes with restriction: AEval|p ≃ AEval$$

Lean4

theorem of_symm_X_smul (m : AEval' φ) : (AEval'.of φ).symm ((X : R[X]) • m) = φ ((AEval'.of φ).symm m) :=
  AEval.of_symm_X_smul _ _

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

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

Разделы

Аффилиация

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