A logical approach to abstract algebra
From MaRDI portal
Publication:3422024
DOI10.1017/S0960129506005627zbMath1118.03059MaRDI QIDQ3422024
Thierry Coquand, Henri Lombardi
Publication date: 9 February 2007
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Projective and free modules and ideals in commutative rings (13C10) Applications of logic to commutative algebra (13L05) Other constructive mathematics (03F65)
Related Items
A universal Krull-Lindenbaum theorem ⋮ Spectral schemes as ringed lattices ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ A universal algorithm for Krull's theorem ⋮ The basic Zariski topology ⋮ Eliminating disjunctions by disjunction elimination ⋮ Maximal elements with minimal logic ⋮ Valuative Lattices and Spectra ⋮ ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION ⋮ Valuative dimension, constructive points of view ⋮ Spectral Spaces Versus Distributive Lattices: A Dictionary ⋮ A formal proof of the projective Eisenbud-Evans-Storch theorem ⋮ A constructive notion of codimension ⋮ A mechanized proof of the basic perturbation lemma ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Constructive finite free resolutions ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ On the Constructive and Computational Content of Abstract Mathematics ⋮ Constructing Gröbner bases for Noetherian rings ⋮ On some peculiar aspects of the constructive theory of point-free spaces ⋮ Un anneau de Prüfer ⋮ Space of valuations ⋮ Noetherian orders ⋮ Cut elimination for entailment relations ⋮ Towards formal Baer criteria ⋮ Maximal ideals in countable rings, constructively ⋮ Syntax for Semantics: Krull’s Maximal Ideal Theorem