mathlib

747aaae9 - chore(algebra/lie/basic): Add some missing simp lemmas about A →ₗ⁅R⁆ B (#4912)

chore(algebra/lie/basic): Add some missing simp lemmas about A →ₗ⁅R⁆ B (#4912) These are mostly inspired by lemmas in linear_map. All the proofs are either `rfl` or copied from a proof for `linear_map`.