conjugation): reverse and involute are grade-preserving (#12373)

Commit

3 years ago

feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving (#12373) This shows that various submodules are preserved under `submodule.map` by `reverse` or `involute`.

Author

eric-wieser

Parents

ac28ddf7

mathlib3 f5b885b0 - feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving (#12373)

mathlib3
f5b885b0 - feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving (#12373)