Theorem AlgCat.forget₂_ringCat_map

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_map View on Github →