Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-03 07:35 383dd2bd

View on Github →

chore(data/equiv): add missing simp lemmas about mk (#6505) This adds missing mk_coe lemmas, and new symm_mk, symm_bijective, and mk_coe' lemmas.

Estimated changes

added theorem alg_equiv.coe_mk
deleted theorem alg_equiv.mk_apply
added theorem alg_equiv.mk_coe'
added theorem alg_equiv.mk_coe
added theorem alg_equiv.symm_mk
modified theorem alg_equiv.symm_symm
deleted theorem alg_equiv.to_fun_apply
added theorem alg_hom.to_fun_eq_coe
added theorem linear_equiv.mk_coe'
added theorem linear_equiv.mk_coe
added theorem linear_equiv.symm_mk
deleted theorem mul_equiv.coe_symm_mk
added theorem mul_equiv.mk_coe'
added theorem mul_equiv.mk_coe
added theorem mul_equiv.symm_mk
added theorem mul_equiv.symm_symm
added theorem ring_equiv.coe_mk
deleted theorem ring_equiv.coe_symm_mk
added theorem ring_equiv.mk_coe'
added theorem ring_equiv.mk_coe
added theorem ring_equiv.symm_mk