charP

Mathlib.Algebra.CharP.IntermediateField

URI: https://scilib.ai/kg/mathlib#Subfield.charP

English

If F is a field of characteristic p and L is a subfield of F, then L has characteristic p as well.

Русский

Если F — поле характеристик p и L — подполе F, то и у L характеристика p.

LaTeX

$$$CharP(F,p) \Rightarrow CharP(L,p)$$$

Lean4

instance charP [CharP F p] : CharP L p :=
  RingHom.charP _ (algebraMap _ F).injective p

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

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

Разделы

Аффилиация

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