Commit 2024-06-28 15:55 dfc07f1b

View on Github →

perf (Algebra.AddConstMap): scope simp lemmas (#14233) The keys for these simp lemmas will match quite a bit. To avoid this, we scope them to the AddConstMapClass namespace so that you only have them when you need them and not when you don't.

Estimated changes

Modified Mathlib/Algebra/AddConstMap/Basic.lean

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