module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671)

Commit

3 years ago

feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671) This is then used to show the even and odd components of a clifford algebra are complementary.

Author

eric-wieser

Parents

90f0bee6

mathlib3 e92ecffc - feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671)

mathlib3
e92ecffc - feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671)