instExpChar

Mathlib.FieldTheory.SplittingField.Construction

URI: https://scilib.ai/kg/mathlib#Polynomial.SplittingField.instExpChar

English

If K has ExpChar p, then the splitting field f.SplittingField has ExpChar p as well.

Русский

Если у поля K есть ExpChar p, то и развертывающее поле f имеет ExpChar p.

LaTeX

$$$\operatorname{ExpChar}(K)=p \Rightarrow \operatorname{ExpChar}(\mathrm{SplittingField}(f),p)$$$

Lean4

instance instExpChar (p : ℕ) [ExpChar K p] : ExpChar (SplittingField f) p :=
  expChar_of_injective_algebraMap (algebraMap K _).injective p

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

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

Разделы

Аффилиация

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