algHomOfDvd_root

Mathlib.RingTheory.AdjoinRoot

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

← MathLib Explorer

English

The map algHomOfDvd sends root f to root g when g|f.

Русский

Отображение algHomOfDvd отправляет корень f в корень g, если g делит f.

LaTeX

$$algHomOfDvd f g hgf (root f) = root g$$

Lean4

/-- `algHomOfDvd` sends `AdjoinRoot.root f` to `AdjoinRoot.root q`. -/
@[simp]
theorem algHomOfDvd_root (f g : R[X]) (hgf) : algHomOfDvd f g hgf (root f) = root g := by rw [algHomOfDvd, liftHom_root]

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

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

Разделы

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

Аффилиация

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