Theorem AlgCat.forget₂_ringCat_obj

Modification history

2026-05-28 22:31
Mathlib/Algebra/Category/AlgCat/Basic.lean
feat(Algebra/Category): filtered colimits in `AlgCat` (#39145) …
Added AlgCat.forget₂_ringCat_objView on Github →