Category Archives: Commutative Algebra

Commutative algebra is a branch of algebra that studies commutative rings, their ideals, and modules over such rings. It provides the algebraic foundation for algebraic geometry and number theory. Topics Covered Ring Polynomial Ring Affine Algebraic Varieties Modules Tensor Product Localization Noetherian and Artinian Rings Continue reading →

Note that all rings considered here are commutative and have a multiplicative identity. Each written proof or proof sketch is followed by a separate folded Lean 4 proof. The snippets are collected and compiled in mathlib-in-lean/commutative-algebra/Ring.lean . They assume that file’s imports, namespace CommAlg , and variable {A : Type*}… Continue reading →