smul_X

Mathlib.Algebra.Polynomial.GroupRingAction

URI: https://scilib.ai/kg/mathlib#Polynomial.smul_X

English

For any monoid action on a semiring R, the polynomial X is fixed by the action: m • X = X.

Русский

Пусть действует моноид M на R; многочлен X инвариантен относительно действия: m • X = X.

LaTeX

$$$\forall m,\ m \cdot X = X$.$$

Lean4

@[simp]
theorem smul_X (m : M) : (m • X : R[X]) = X :=
  (smul_eq_map R m).symm ▸ map_X _

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

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

Разделы

Аффилиация

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