Commutative algebra

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.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.function-commutative-rings public
open import commutative-algebra.function-commutative-semirings public
open import commutative-algebra.gaussian-integers 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.integral-domains public
open import commutative-algebra.invertible-elements-commutative-rings public
open import commutative-algebra.isomorphisms-commutative-rings public
open import commutative-algebra.local-commutative-rings public
open import commutative-algebra.maximal-ideals-commutative-rings public
open import commutative-algebra.nilradical-commutative-rings public
open import commutative-algebra.nilradicals-commutative-semirings 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.radical-ideals-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.trivial-commutative-rings public
open import commutative-algebra.zariski-topology public