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 : ℕ) :
Language.ring.Sentence

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] [Ring.CompatibleRing K] (n : ℕ) (v : Empty → K) :
      Language.Formula.Realize (eqZero n) v ↔ ↑n = 0
      source
      def FirstOrder.Language.Theory.fieldOfChar (p : ℕ) :
      ring.Theory

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

      Equations
        Instances For
          source
          instance FirstOrder.Field.model_hasChar_of_charP {p : ℕ} {K : Type u_1} [Field K] [Ring.CompatibleRing K] [CharP K p] :
          K ⊨ Language.Theory.fieldOfChar p
          source
          theorem FirstOrder.Field.charP_iff_model_fieldOfChar {p : ℕ} {K : Type u_1} [Field K] [Ring.CompatibleRing K] :
          K ⊨ Language.Theory.fieldOfChar p ↔ CharP K p
          source
          instance FirstOrder.Field.model_fieldOfChar_of_charP {p : ℕ} {K : Type u_1} [Field K] [Ring.CompatibleRing K] [CharP K p] :
          K ⊨ Language.Theory.fieldOfChar p
          source
          theorem FirstOrder.Field.charP_of_model_fieldOfChar (p : ℕ) (K : Type u_1) [Field K] [Ring.CompatibleRing K] [h : K ⊨ Language.Theory.fieldOfChar p] :
          CharP K p