Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-20 00:07 d7a8709e

View on Github →

chore(algebra/group/hom): Add mk_coe lemmas (#5812) These are the counterparts to the coe_mk lemmas.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_hom.mk_coe

Modified src/algebra/group/hom.lean

added theorem monoid_hom.mk_coe

added theorem monoid_with_zero_hom.mk_coe

added theorem mul_hom.mk_coe

added theorem one_hom.mk_coe

Modified src/algebra/module/linear_map.lean

added theorem linear_map.mk_coe

Modified src/algebra/ring/basic.lean

added theorem ring_hom.mk_coe