Commit 2023-05-27 09:19 aabb3054

View on Github →

feat: port Algebra.Category.Ring.Adjunctions (#4413)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Ring/Adjunctions.lean

added def CommRingCat.adj

added def CommRingCat.free

added theorem CommRingCat.free_map_coe

added theorem CommRingCat.free_obj_coe