Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 09:10 f5b885b0

View on Github →

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.

Estimated changes

Modified src/linear_algebra/clifford_algebra/conjugation.lean

added theorem clifford_algebra.even_odd_comap_involute

added theorem clifford_algebra.even_odd_comap_reverse

added theorem clifford_algebra.even_odd_map_involute

added theorem clifford_algebra.even_odd_map_reverse

added theorem clifford_algebra.involute_mem_even_odd_iff

added theorem clifford_algebra.reverse_mem_even_odd_iff

added theorem clifford_algebra.submodule_comap_mul_reverse

added theorem clifford_algebra.submodule_comap_pow_reverse

added theorem clifford_algebra.submodule_map_involute_eq_comap

added theorem clifford_algebra.submodule_map_mul_reverse

added theorem clifford_algebra.submodule_map_pow_reverse

added theorem clifford_algebra.submodule_map_reverse_eq_comap

Modified src/linear_algebra/clifford_algebra/grading.lean

added theorem clifford_algebra.ι_mem_even_odd_one