Ring theory

Files in the ring theory folder

module ring-theory where

open import ring-theory.algebras-rings public
open import ring-theory.binomial-theorem-rings public
open import ring-theory.binomial-theorem-semirings public
open import ring-theory.central-elements-rings public
open import ring-theory.central-elements-semirings public
open import ring-theory.congruence-relations-rings public
open import ring-theory.congruence-relations-semirings public
open import ring-theory.dependent-products-rings public
open import ring-theory.dependent-products-semirings public
open import ring-theory.division-rings public
open import ring-theory.function-rings public
open import ring-theory.function-semirings public
open import ring-theory.homomorphisms-rings public
open import ring-theory.homomorphisms-semirings public
open import ring-theory.ideals-generated-by-subsets-rings public
open import ring-theory.ideals-rings public
open import ring-theory.ideals-semirings public
open import ring-theory.idempotent-elements-rings public
open import ring-theory.invariant-basis-property-rings public
open import ring-theory.invertible-elements-rings public
open import ring-theory.isomorphisms-rings public
open import ring-theory.local-rings public
open import ring-theory.localizations-rings public
open import ring-theory.maximal-ideals-rings public
open import ring-theory.modules-rings public
open import ring-theory.nil-ideals-rings public
open import ring-theory.nilpotent-elements-rings public
open import ring-theory.nilpotent-elements-semirings public
open import ring-theory.opposite-rings public
open import ring-theory.powers-of-elements-rings public
open import ring-theory.powers-of-elements-semirings public
open import ring-theory.precategory-of-rings public
open import ring-theory.precategory-of-semirings public
open import ring-theory.products-rings public
open import ring-theory.quotient-rings public
open import ring-theory.radical-ideals-rings public
open import ring-theory.rings public
open import ring-theory.semirings public
open import ring-theory.subsets-rings public
open import ring-theory.subsets-semirings public
open import ring-theory.sums-rings public
open import ring-theory.sums-semirings public
open import ring-theory.trivial-rings public