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
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[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
    🔸 coverage
    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

    Instances For
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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