Commit 2024-07-19 00:25 966e2d6e

View on Github →

feat: define AddConstEquiv (#9726) Also revert some scoped modifiers on simps.

Estimated changes

modified theorem AddConstMap.coe_mk
modified theorem AddConstMap.coe_mul
modified theorem AddConstMap.coe_one
modified theorem AddConstMap.coe_pow
modified theorem AddConstMap.comp_id
modified theorem AddConstMap.conjNeg_symm
modified theorem AddConstMap.id_comp
modified theorem AddConstMap.mk_coe
modified theorem AddConstMap.toFun_eq_coe
added theorem AddConstEquiv.ext
added structure AddConstEquiv