charP_of_model_fieldOfChar

Mathlib.ModelTheory.Algebra.Field.CharP

URI: https://scilib.ai/kg/mathlib#FirstOrder.Field.charP_of_model_fieldOfChar

English

If K is a field and there exists a model for fieldOfChar p on K, then CharP K p holds.

Русский

Если K — поле и существует модель fieldOfChar p на K, тогда CharP K p верна.

LaTeX

$$charP_of_model_fieldOfChar : (Theory.fieldOfChar p).Model K ⇒ CharP K p$$

Lean4

theorem charP_of_model_fieldOfChar [Field K] [CompatibleRing K] [h : (Theory.fieldOfChar p).Model K] : CharP K p :=
  charP_iff_model_fieldOfChar.1 h

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

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

Разделы

Аффилиация

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