Commit 2021-02-22 21:32 c0389845

View on Github →

chore(data/equiv/*): add missing coercion lemmas for equivs (#6268) This does not affect the simp-normal form. This tries to make a lot of lemma names and statements more consistent:

restates linear_map.mk_apply to be linear_map.coe_mk to match monoid_hom.coe_mk
adds linear_map.to_linear_map_eq_coe
adds the simp lemma linear_map.coe_to_equiv
adds the simp lemma linear_map.linear_map.coe_to_linear_map
adds the simp lemma linear_map.to_fun_eq_coe
adds the missing ancestor attributes required to make to_additive work for things like add_equiv.to_add_hom
restates add_equiv.to_fun_apply to be add_equiv.to_fun_eq_coe
restates add_equiv.to_equiv_apply to be add_equiv.coe_to_equiv
adds the simp lemma add_equiv.coe_to_mul_hom
removes add_equiv.to_add_monoid_hom_apply since add_equiv.coe_to_add_monoid_hom is a shorter and more general statement
restates ring_equiv.to_fun_apply to be ring_equiv.to_fun_eq_coe
restates ring_equiv.coe_mul_equiv to be ring_equiv.coe_to_mul_equiv
restates ring_equiv.coe_add_equiv to be ring_equiv.coe_to_add_equiv
restates ring_equiv.coe_ring_hom to be ring_equiv.coe_to_ring_hom
adds ring_equiv.to_ring_hom_eq_coe
adds ring_equiv.to_add_equiv_eq_coe
adds ring_equiv.to_mul_equiv_eq_coe