[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star (star x) = x
[PROOFSTEP]
simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
⊢ star (x * y) = star y * star x
[PROOFSTEP]
simp only [map_mul, reverse.map_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
⊢ star (x + y) = star x + star y
[PROOFSTEP]
simp only [map_add]
  -- porting note: cannot infer `Q`
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ star (↑(ι Q) m) = -↑(ι Q) m
[PROOFSTEP]
rw [star_def, involute_ι, map_neg, reverse_ι]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
x : CliffordAlgebra Q
⊢ star (r • x) = r • star x
[PROOFSTEP]
rw [star_def, star_def, map_smul, map_smul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ star (↑(algebraMap R (CliffordAlgebra Q)) r) = ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
rw [star_def, involute.commutes, reverse.commutes]
