Algebra

Extensions of Mathlib's Algebra/, at Mathlib's paths: ring, module, and polynomial algebra; the concrete algebraic categories under Category/; and homological algebra under Homology/, including derived categories, the homotopy category and its dg enhancement, spectral sequences, and dg categories; and, under Order/, the group of order automorphisms of ℝ commuting with unit translation.