Nothing

leanprover-community · Oct 20, 2022 · a9b386d · a9b386d
1 parent 4179e43
commit a9b386d
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/linear_algebra/clifford_algebra/spin_group.lean b/src/linear_algebra/clifford_algebra/spin_group.lean
@@ -376,8 +376,7 @@ instance : group (spin_group Q) :=
   mul_left_inv := star_mul_self,
   ..submonoid.to_monoid _ }
 
-instance : has_involutive_star (spin_group Q) :=
-⟨λ _, by { ext, simp only [coe_star, star_star] }⟩
+instance : has_involutive_star (spin_group Q) := ⟨λ _, by { ext, simp only [coe_star, star_star] }⟩
 
 instance : star_semigroup (spin_group Q) :=
 ⟨λ _ _, by { ext, simp only [coe_star, submonoid.coe_mul, star_mul] }⟩