Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-09 22:44 d692499e

View on Github →

reorganising category_theory/instances/rings.lean (#909)

Estimated changes

Created src/category_theory/instances/CommRing/adjunctions.lean

added theorem category_theory.instances.CommRing.polynomial_ring_map_val

added theorem category_theory.instances.CommRing.polynomial_ring_obj_α

Renamed src/category_theory/instances/rings.lean to src/category_theory/instances/CommRing/basic.lean

deleted theorem category_theory.instances.CommRing.polynomial_map_val

deleted theorem category_theory.instances.CommRing.polynomial_obj_α

Created src/category_theory/instances/CommRing/default.lean