Mathlib v3 is deprecated. Go to Mathlib v4

Theorem clifford_algebra.even_odd_is_compl

Modification history

2022-03-29 17:44
src/linear_algebra/clifford_algebra/grading.lean
feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671) …
Added clifford_algebra.even_odd_is_complView on Github →