Documentation

Mathlib.ModelTheory.Algebra.Field.Basic

The First Order Theory of Fields #

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

Main definitions #

An indexing type to name each of the field axioms. The theory of fields is defined as the range of a function FieldAxiom -> Language.ring.Sentence

Instances For

    The first order sentence corresponding to each field axiom

    Equations
    Instances For

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

      Equations
      Instances For
        @[reducible, inline]

        A model for the theory of fields is a field. To introduced locally on Types that don't already have instances for ring operations.

        When this is used, it is almost always useful to also add locally the instance compatibleFieldOfModelField afterwards.

        Equations
        Instances For
          @[reducible, inline]

          The instances given by fieldOfModelField are compatible with the Language.ring.Structure instance on K. This instance is to be used on models for the language of fields that do not already have the ring operations on the Type.

          Always add fieldOfModelField as a local instance first before using this instance.

          Equations
          Instances For