expChar'

Mathlib.Algebra.CharP.IntermediateField

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

English

If F, E are fields with F → E, and L is an IntermediateField F E, then ExpChar L p holds provided ExpChar E p holds.

Русский

Если F и E — поля, имеется включение F → E, и L — промежуточное поле F E, то ExpChar L p держится при ExpChar E p.

LaTeX

$$$ExpChar L p$$$

Lean4

instance expChar' [ExpChar E p] : ExpChar L p :=
  Subfield.expChar L.toSubfield p

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

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

Разделы

Аффилиация

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