Commit 2020-05-07 13:09 6c484441
View on Github →feat(algebra/lie_algebra): lie_algebra.of_associative_algebra is functorial (#2620)
More precisely we:
- define the Lie algebra homomorphism associated to a morphism of associative algebras
- prove that the correspondence is functorial
- prove that subalgebras and Lie subalgebras correspond