smul_of

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.smul_of

← MathLib Explorer

English

The action of S on AdjoinRoot f commutes with the embedding of R, i.e., a · of f x = of f (a · x) for a ∈ S and x ∈ R.

Русский

Действие S на AdjoinRoot f commute с вложением R: a · of f x = of f (a · x).

LaTeX

$$$a \\cdot of f x = of f (a \\cdot x)$$$

Lean4

theorem smul_of [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) : a • of f x = of f (a • x) := by
  rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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