theorem SOAction.isometry_det_sq_eq_one {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hnd : B.Nondegenerate) (g : V ≃ₗ[k] V) (hiso : ∀ (v w : V), (B (g v)) (g w) = (B v) w) : LinearMap.det ↑g ^ 2 = 1

The determinant of any isometry of a nondegenerate bilinear form satisfies $(\det g)^2 = 1$.

theorem SOAction.isometry_det_eq_one_or_neg_one {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hnd : B.Nondegenerate) (g : V ≃ₗ[k] V) (hiso : ∀ (v w : V), (B (g v)) (g w) = (B v) w) : LinearMap.det ↑g = 1 ∨ LinearMap.det ↑g = -1

An isometry of a nondegenerate bilinear form has determinant $\pm 1$.

def SOAction.SpecialIsometryGroup {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Set (V ≃ₗ[k] V)

The special isometry group $\mathrm{SO}(B)$: isometries of $B$ with determinant 1.

theorem SOAction.hyp_swap_det_neg_one {k : Type u_1} [Field k] : !![0, 1; 1, 0].det = -1

The $2 \times 2$ swap matrix has determinant $-1$.

theorem SOAction.hyp_plane_swap_isometry_det {k : Type u_1} [Field k] (e₁ e₂ : Fin 2 → k) (b : Module.Basis (Fin 2) k (Fin 2 → k)) (hb1 : b 0 = e₁) (hb2 : b 1 = e₂) (g : (Fin 2 → k) ≃ₗ[k] Fin 2 → k) (a : k) (ha : a ≠ 0) (hge1 : g e₁ = a • e₂) (hge2 : g e₂ = a⁻¹ • e₁) : LinearMap.det ↑g = -1

An isometry of a hyperbolic plane $(e_1, e_2)$ which sends $e_1 \mapsto a e_2$ and $e_2 \mapsto a^{-1} e_1$ has determinant $-1$.