rootsExpandEquivRoots_apply

Mathlib.FieldTheory.Perfect

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

English

The Apply lemma confirms the p^n-th power relation on the representative.

Русский

Лемма применения подтверждает отношение степени p^n для представителя.

LaTeX

$$$\text{rootsExpandPowEquivRoots_apply }(p,f,n,x) : (\text{representative}) = x^{p^n}$$$

Lean4

@[simp]
theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p :=
  rfl

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

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

Разделы

Аффилиация

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