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