rootsExpandToRoots_apply

Mathlib.FieldTheory.Perfect

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

English

There is a canonical map from roots of expand R p f to roots of f given by x ↦ x^p.

Русский

Существуют естественная отображение от корней expand R p f к корням f, задаваемое x ↦ x^p.

LaTeX

$$$\bigl(\mathrm{rootsExpandToRoots}\; p\; f\bigr)(x) = x^{p}$$$

Lean4

@[simp]
theorem rootsExpandToRoots_apply (x) : (rootsExpandToRoots p f x : R) = x ^ p :=
  rfl

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

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

Разделы

Аффилиация

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