Documentation

Mathlib.ModelTheory.Algebra.Field.CharP

First order theory of fields #

This file defines the first order theory of fields of characteristic p as a theory over the language of rings

Main definitions #

source
noncomputable def FirstOrder.Field.eqZero (n : ℕ) :
FirstOrder.Language.Sentence FirstOrder.Language.ring

For a given natural number n, eqZero n is the sentence in the language of rings saying that n is zero.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Field.realize_eqZero {K : Type u_1} [CommRing K] [FirstOrder.Ring.CompatibleRing K] (n : ℕ) (v : Empty → K) :
    FirstOrder.Language.Formula.Realize (FirstOrder.Field.eqZero n) v ↔ ↑n = 0
    source
    def FirstOrder.Language.Theory.fieldOfChar (p : ℕ) :
    FirstOrder.Language.Theory FirstOrder.Language.ring

    The first order theory of fields of characteristic p as a theory over the language of rings

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance FirstOrder.Field.model_hasChar_of_charP {p : ℕ} {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] [CharP K p] :
      K ⊨ FirstOrder.Language.Theory.fieldOfChar p
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem FirstOrder.Field.charP_iff_model_fieldOfChar {p : ℕ} {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] :
      K ⊨ FirstOrder.Language.Theory.fieldOfChar p ↔ CharP K p
      source
      instance FirstOrder.Field.model_fieldOfChar_of_charP {p : ℕ} {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] [CharP K p] :
      K ⊨ FirstOrder.Language.Theory.fieldOfChar p
      Equations
      source
      theorem FirstOrder.Field.charP_of_model_fieldOfChar (p : ℕ) (K : Type u_1) [Field K] [FirstOrder.Ring.CompatibleRing K] [h : K ⊨ FirstOrder.Language.Theory.fieldOfChar p] :
      CharP K p