Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.instances.CommRing.hom_coe_app

Modification history

2019-05-31 06:43
src/algebra/CommRing/basic.lean
chore(category_theory): move all instances (e.g. Top, CommRing, Meas) into the root namespace (#1074) …
Deleted category_theory.instances.CommRing.hom_coe_appView on Github →
2019-05-04 20:01
src/category_theory/instances/CommRing/basic.lean
feat(colimits): arbitrary colimits in Mon and CommRing (#910) …
Modified category_theory.instances.CommRing.hom_coe_appView on Github →
2019-01-30 18:20
src/category_theory/instances/rings.lean
refactor(category_theory/instances): rename `examples` to `instances`
Added category_theory.instances.CommRing.hom_coe_appView on Github →