Conjugations #

This file contains additional lemmas about clifford_algebra.reverse and clifford_algebra.involute.

As more and more goes into Mathlib, this file will become smaller and spaller. The links above will take you to the collection of mathlib theorems.

def clifford_algebra.reverse_aux {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :

Equations

theorem clifford_algebra.reverse_eq_reverse_aux {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :

@[simp]

theorem clifford_algebra.unop_reverse_aux {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) (x : clifford_algebra Q) :

theorem clifford_algebra.reverse_prod_sign_aux {R : Type u_1} [comm_ring R] (n : ℕ) :

(-1) ^ ((n + 1) * (n + 1 + 1) / 2) = (-1) ^ (n * (n + 1) / 2) * (-1) ^ (n + 1)

helper lemma for expanding the sign of reverse

theorem clifford_algebra.reverse_prod_map_sign {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (l : list M) :

TODO: this needs an assumption that the vectors are othogonal

Note: this declaration is incomplete and uses sorry.