subalgebra): define the Lie subalgebra generated by a subset (#6549)

Commit

4 years ago

feat(algebra/lie/subalgebra): define the Lie subalgebra generated by a subset (#6549) The work here is a lightly-edited copy-paste of the corresponding results for Lie submodules

Author

ocfnash

Parents

d90448c6

mathlib3 97d13d75 - feat(algebra/lie/subalgebra): define the Lie subalgebra generated by a subset (#6549)

mathlib3
97d13d75 - feat(algebra/lie/subalgebra): define the Lie subalgebra generated by a subset (#6549)