model_fieldOfChar_of_charP

Mathlib.ModelTheory.Algebra.Field.CharP

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

← MathLib Explorer

English

If K is a field and CharP K p holds, then K models the theory fieldOfChar p.

Русский

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

LaTeX

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

Lean4

instance model_fieldOfChar_of_charP [Field K] [CompatibleRing K] [CharP K p] : (Theory.fieldOfChar p).Model K :=
  charP_iff_model_fieldOfChar.2 inferInstance

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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