Commutative algebra

Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer, Fernando Chu, Jonathan Prieto-Cubides, Victor Blanchi and Gregor Perčič.

Created on 2022-04-22.
Last modified on 2023-09-21.

Files in the commutative algebra folder

module commutative-algebra where

open import commutative-algebra.binomial-theorem-commutative-rings public
open import commutative-algebra.binomial-theorem-commutative-semirings public
open import commutative-algebra.boolean-rings public
open import commutative-algebra.category-of-commutative-rings public
open import commutative-algebra.commutative-rings public
open import commutative-algebra.commutative-semirings public
open import commutative-algebra.dependent-products-commutative-rings public
open import commutative-algebra.dependent-products-commutative-semirings public
open import commutative-algebra.discrete-fields public
open import commutative-algebra.eisenstein-integers public
open import commutative-algebra.euclidean-domains public
open import commutative-algebra.full-ideals-commutative-rings public
open import commutative-algebra.function-commutative-rings public
open import commutative-algebra.function-commutative-semirings public
open import commutative-algebra.gaussian-integers public
open import commutative-algebra.groups-of-units-commutative-rings public
open import commutative-algebra.homomorphisms-commutative-rings public
open import commutative-algebra.homomorphisms-commutative-semirings public
open import commutative-algebra.ideals-commutative-rings public
open import commutative-algebra.ideals-commutative-semirings public
open import commutative-algebra.ideals-generated-by-subsets-commutative-rings public
open import commutative-algebra.integer-multiples-of-elements-commutative-rings public
open import commutative-algebra.integral-domains public
open import commutative-algebra.intersections-ideals-commutative-rings public
open import commutative-algebra.intersections-radical-ideals-commutative-rings public
open import commutative-algebra.invertible-elements-commutative-rings public
open import commutative-algebra.isomorphisms-commutative-rings public
open import commutative-algebra.joins-ideals-commutative-rings public
open import commutative-algebra.joins-radical-ideals-commutative-rings public
open import commutative-algebra.local-commutative-rings public
open import commutative-algebra.maximal-ideals-commutative-rings public
open import commutative-algebra.multiples-of-elements-commutative-rings public
open import commutative-algebra.nilradical-commutative-rings public
open import commutative-algebra.nilradicals-commutative-semirings public
open import commutative-algebra.poset-of-ideals-commutative-rings public
open import commutative-algebra.poset-of-radical-ideals-commutative-rings public
open import commutative-algebra.powers-of-elements-commutative-rings public
open import commutative-algebra.powers-of-elements-commutative-semirings public
open import commutative-algebra.precategory-of-commutative-rings public
open import commutative-algebra.precategory-of-commutative-semirings public
open import commutative-algebra.prime-ideals-commutative-rings public
open import commutative-algebra.products-commutative-rings public
open import commutative-algebra.products-ideals-commutative-rings public
open import commutative-algebra.products-radical-ideals-commutative-rings public
open import commutative-algebra.products-subsets-commutative-rings public
open import commutative-algebra.radical-ideals-commutative-rings public
open import commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings public
open import commutative-algebra.radicals-of-ideals-commutative-rings public
open import commutative-algebra.subsets-commutative-rings public
open import commutative-algebra.subsets-commutative-semirings public
open import commutative-algebra.sums-commutative-rings public
open import commutative-algebra.sums-commutative-semirings public
open import commutative-algebra.transporting-commutative-ring-structure-isomorphisms-abelian-groups public
open import commutative-algebra.trivial-commutative-rings public
open import commutative-algebra.zariski-locale public
open import commutative-algebra.zariski-topology public

Recent changes