Commit 2020-11-06 10:17 747aaae9

View on Github →

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.

Estimated changes

Modified src/algebra/lie/basic.lean

added theorem lie_algebra.coe_mk

added theorem lie_algebra.morphism.coe_injective

modified theorem lie_algebra.morphism.comp_apply

added theorem lie_algebra.morphism.comp_coe

added theorem lie_algebra.morphism.ext_iff

added theorem lie_algebra.of_associative_algebra_hom_apply