feat(LinearAlgebra/UnitaryGroup): special orthogonal group (#11708)

Co-authored-by: Bergschaf <christian.k@netcom-mail.de>
Co-authored-by: bergschaf <christian.k@netcom-mail.de>

Mathlib/LinearAlgebra/UnitaryGroup.lean

@@ -198,6 +198,22 @@ set_option linter.uppercaseLean3 false in
 
 end UnitaryGroup
 
+section specialUnitaryGroup
+
+variable (n) (α)
+
+/--`Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant
+is 1. (This definition is only correct if 2 is invertible.)-/
+abbrev specialUnitaryGroup := unitaryGroup n α ⊓ MonoidHom.mker detMonoidHom
+
+variable {n} {α}
+
+theorem mem_specialUnitaryGroup_iff :
+    A ∈ specialUnitaryGroup n α ↔ A ∈ unitaryGroup n α ∧ A.det = 1 :=
+  Iff.rfl
+
+end specialUnitaryGroup
+
 section OrthogonalGroup
 
 variable (n) (β : Type v) [CommRing β]
@@ -226,4 +242,22 @@ theorem mem_orthogonalGroup_iff' {A : Matrix n n β} :
 
 end OrthogonalGroup
 
+section specialOrthogonalGroup
+
+variable (n) (β : Type v) [CommRing β]
+
+attribute [local instance] starRingOfComm
+
+/-- `Matrix.specialOrthogonalGroup n` is the group of orthogonal `n` by `n` where the determinant
+is one. (This definition is only correct if 2 is invertible.)-/
+abbrev specialOrthogonalGroup := specialUnitaryGroup n β
+
+variable {n} {β} {A : Matrix n n β}
+
+theorem mem_specialOrthogonalGroup_iff :
+    A ∈ specialOrthogonalGroup n β ↔ A ∈ orthogonalGroup n β ∧ A.det = 1 :=
+  Iff.rfl
+
+end specialOrthogonalGroup
+
 end Matrix