X_smul_of

Mathlib.Algebra.Polynomial.Module.AEval

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

English

AEval' φ is identical to AEval R M φ as R-modules.

Русский

AEval' φ идентичен AEval R M φ как R-модуль.

LaTeX

$$$\text{AEval}'\; φ = AEval\; R\ M\ φ$$$

Lean4

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

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

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

Разделы

Аффилиация

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