direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369)

Commit

4 years ago

feat(algebra/lie/direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369) Various other minor improvements.

Author

ocfnash

Parents

df50b6c2

mathlib3 c9593dcc - feat(algebra/lie/direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369)

mathlib3
c9593dcc - feat(algebra/lie/direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369)