Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-26 13:12 fb6046ed

View on Github →

feat(/category/): add coe_of simp lemmas (#3938)

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

added theorem Algebra.coe_of

deleted theorem Algebra.of_apply

Modified src/algebra/category/CommRing/basic.lean

added theorem CommRing.coe_of

added theorem CommSemiRing.coe_of

added theorem Ring.coe_of

added theorem SemiRing.coe_of

Modified src/algebra/category/Group/basic.lean

added theorem CommGroup.coe_of

added theorem Group.coe_of

Modified src/algebra/category/Module/basic.lean

added theorem Module.coe_of

deleted theorem Module.of_apply

Modified src/algebra/category/Mon/basic.lean

added theorem CommMon.coe_of

added theorem Mon.coe_of

Modified src/measure_theory/category/Meas.lean

added theorem Meas.coe_of

Modified src/topology/category/Top/basic.lean

added theorem Top.coe_of

Modified src/topology/category/TopCommRing.lean

added theorem TopCommRing.coe_of

Modified src/topology/category/UniformSpace.lean

added theorem CpltSepUniformSpace.coe_of

added theorem UniformSpace.coe_of