Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-03 21:31
2fc2d1b6
View on Github →
feat(linear_algebra/clifford_algebra): lemmas about mapping submodules (
#12399
)
Estimated changes
Modified
src/linear_algebra/basic.lean
added
theorem
linear_map.range_neg
Modified
src/linear_algebra/clifford_algebra/basic.lean
added
theorem
clifford_algebra.ι_range_map_lift
added
theorem
clifford_algebra.ι_range_map_map
Modified
src/linear_algebra/clifford_algebra/conjugation.lean
added
def
clifford_algebra.involute_equiv
added
def
clifford_algebra.reverse_equiv
added
theorem
clifford_algebra.ι_range_comap_involute
added
theorem
clifford_algebra.ι_range_comap_reverse
added
theorem
clifford_algebra.ι_range_map_involute
added
theorem
clifford_algebra.ι_range_map_reverse