Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Regular Element Property in Constructive Mathematics

Thierry Coquand

Abstract

The goal of this note is to present Kaplansky's proof of the Regular Element Property and to explain how this argument can be adapted to the case of a coherent, strongly discrete and Noetherian (with an inductive definition of Noetherian) rings in a constructive setting. We thus get, in this setting, an algorithm which given a f.g. regular ideal, build a regular element in this ideal.

The Regular Element Property in Constructive Mathematics

Abstract

The goal of this note is to present Kaplansky's proof of the Regular Element Property and to explain how this argument can be adapted to the case of a coherent, strongly discrete and Noetherian (with an inductive definition of Noetherian) rings in a constructive setting. We thus get, in this setting, an algorithm which given a f.g. regular ideal, build a regular element in this ideal.
Paper Structure (2 sections, 4 theorems)

This paper contains 2 sections, 4 theorems.

Table of Contents

  1. Classical Proof
  2. Constructive Version

Key Result

Lemma 2.0.1

The relation $\prec$ is well-founded.

Theorems & Definitions (7)

  • Lemma 2.0.1
  • proof
  • Corollary 2.0.1
  • proof
  • Lemma 2.0.2
  • proof
  • Lemma 2.0.3