\( \DeclareMathOperator{\tr}{tr} \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} % For +---- metric \newcommand{\BDpos}{} \newcommand{\BDneg}{-} \newcommand{\BDposs}{\phantom{-}} \newcommand{\BDnegg}{-} \newcommand{\BDplus}{+} \newcommand{\BDminus}{-} % For -+++ metric \newcommand{\BDpos}{-} \newcommand{\BDposs}{-} \newcommand{\BDneg}{} \newcommand{\BDnegg}{\phantom{-}} \newcommand{\BDplus}{-} \newcommand{\BDminus}{+} \)
UP | HOME

Ring Theory - Mizar

Table of Contents

1. Overview

This is just a "map" or "analytical table of contents", of where things are defined in the "ring theory wing" of the Mizar library.

The articles of interest include RING_* articles, as well as VECTSP_* articles (for fields and whatnot).

  • polynom3 defines:
    • Polynomial of L as AlgSequence of L
    • Polynom-Ring L is a stricct doubleLoopStr (which is then proved to be a ring through registrations)
  • In polyalg1, we have the following definitions
    • Algebra over F (which is both a "ring" (doubleLoopStr) and a ModuleStr over F)
    • Subalgebra
  • In vectsp_1:
    • Ring
    • Skew-Field
    • Field
    • ModuleStr
    • VectSp
  • In vectsp_2:
    • RightModStr
    • LeftModStr
    • BiModStr
    • comRing is an abbreviation for commutative Ring
    • domRing is an abbreviation for domRing-like Ring (which appears to be a ring with no zero divisors).
  • ring_1 defines quotient rings
  • ideal_1 defines the notion of an ideal for a double loop
  • ring_3 defines the characteristic of rings, and some stuff about prime fields
  • ringfrac defines the ring of fractions and localization, for commutative rings
  • ec_pf_1 (Set of Points on Elliptic Curve in Projective Coordinates)

1.1. Familiar Fields

  • complfld defines F_Complex the field of complex numbers (whose underlying set is COMPLEX, the set of complex numbers)
  • F_Real (the field of real numbers) is defined in vectsp_1
  • F_Rat is the field of rational numbers
  • Gauss_INT_Field is the field of Gaussian integers, as defined in gaussint
  • INT.Ring is the ring of integers \(\mathbb{Z}\) (INT_3:def 3)
  • INT.Ring n is the ring \(\mathbb{Z}/n\mathbb{Z}\) (defined in INT_3:def 12)

Last Updated: Wed, 4 May 2022 12:58:46 -0700