expChar

Mathlib.Algebra.CharP.IntermediateField

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

English

If F is a field and L is a subfield of F, then ExpChar L p holds whenever ExpChar F p holds.

Русский

Если F — поле и L — подполе F, то ExpChar L p выполняется при ExpChar F p.

LaTeX

$$$ExpChar(L,p)$$$

Lean4

instance expChar [ExpChar F p] : ExpChar L p :=
  RingHom.expChar _ (algebraMap _ F).injective p

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

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

Разделы

Аффилиация

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