Commit 2023-06-23 06:08 ef690afb

feat: port LinearAlgebra.CliffordAlgebra.Conjugation (#5404) Annoyingly, Lean 4 cannot work out that reverse x where x : clifford_algebra Q is referring to reverse (Q := Q) x, even though that's the only thing that type checks. Otherwise the only difficulty when porting was the standard LinearMap.range dot notation failing thing.