charP'

Mathlib.Algebra.CharP.IntermediateField

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

English

If E is a field with CharP E p and L is an IntermediateField F E, then CharP L p holds via Subfield transfer.

Русский

Если E — поле с CharP E p и L — промежуточное поле F E, то CharP L p следует через перенос подполей.

LaTeX

$$$CharP L p$$$

Lean4

instance charP' [CharP E p] : CharP L p :=
  Subfield.charP L.toSubfield p

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

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

Разделы

Аффилиация

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