instFinitePolynomialAEval'

Mathlib.Algebra.Polynomial.Module.AEval

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

English

The symmetric action of X on AEval' corresponds to φ acting on the symmetric preimage.

Русский

Симметричное действие X на AEval' соответствует действию φ на обратное изображение.

LaTeX

$$$(AEval'.of φ)^{-1} (X\cdot m) = φ^{-1} (m)$$$

Lean4

instance [Module.Finite R M] : Module.Finite R[X] <| AEval' φ :=
  inferInstance

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

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

Разделы

Аффилиация

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