Ring theory

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

Created on 2022-03-12.
Last modified on 2024-09-23.

Modules in the ring theory namespace

module ring-theory where

open import ring-theory.additive-orders-of-elements-rings public
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.category-of-cyclic-rings public
open import ring-theory.category-of-rings public
open import ring-theory.central-elements-rings public
open import ring-theory.central-elements-semirings public
open import ring-theory.characteristics-rings public
open import ring-theory.commuting-elements-rings public
open import ring-theory.congruence-relations-rings public
open import ring-theory.congruence-relations-semirings public
open import ring-theory.cyclic-rings 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.free-rings-with-one-generator public
open import ring-theory.full-ideals-rings public
open import ring-theory.function-rings public
open import ring-theory.function-semirings public
open import ring-theory.generating-elements-rings public
open import ring-theory.groups-of-units-rings public
open import ring-theory.homomorphisms-cyclic-rings 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.initial-rings public
open import ring-theory.integer-multiples-of-elements-rings public
open import ring-theory.intersections-ideals-rings public
open import ring-theory.intersections-ideals-semirings 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.joins-ideals-rings public
open import ring-theory.joins-left-ideals-rings public
open import ring-theory.joins-right-ideals-rings public
open import ring-theory.kernels-of-ring-homomorphisms public
open import ring-theory.left-ideals-generated-by-subsets-rings public
open import ring-theory.left-ideals-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.multiples-of-elements-rings public
open import ring-theory.multiplicative-orders-of-units-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.poset-of-cyclic-rings public
open import ring-theory.poset-of-ideals-rings public
open import ring-theory.poset-of-left-ideals-rings public
open import ring-theory.poset-of-right-ideals-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-ideals-rings public
open import ring-theory.products-left-ideals-rings public
open import ring-theory.products-right-ideals-rings public
open import ring-theory.products-rings public
open import ring-theory.products-subsets-rings public
open import ring-theory.quotient-rings public
open import ring-theory.radical-ideals-rings public
open import ring-theory.right-ideals-generated-by-subsets-rings public
open import ring-theory.right-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.transporting-ring-structure-along-isomorphisms-abelian-groups public
open import ring-theory.trivial-rings public

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
• 2023-09-11. Egbert Rijke. The categories of rings and commutative rings (#750).
• 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
• 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).