charZero

Mathlib.Algebra.CharP.IntermediateField

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

English

If F and E are fields with an algebra F → E and L is an IntermediateField F E, and F has CharZero, then CharZero L holds.

Русский

Если F и E — поля, имеется отображение F → E, L — промежуточное поле F E, и F имеет CharZero, то L имеет CharZero.

LaTeX

$$$CharZero L$$$

Lean4

instance charZero [CharZero F] : CharZero L :=
  charZero_of_injective_algebraMap (algebraMap F _).injective

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

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

Разделы

Аффилиация

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