expChar

Mathlib.Algebra.CharP.IntermediateField

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

English

If F is a field with ExpChar F p, then ExpChar L p holds for the IntermediateField L ≤ F.

Русский

Если F — поле с ExpChar p, то для промежуточного поля L ≤ F выполняется ExpChar L p.

LaTeX

$$$ExpChar L p$$$

Lean4

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

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

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

Разделы

Аффилиация

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