theorem Garrett.isometry_det_eq_one_or_neg_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] [NoZeroDivisors R] {Q g : Matrix n n R} (hQ : Q.det ≠ 0) (hiso : g.transpose * Q * g = Q) : g.det = 1 ∨ g.det = -1

A matrix isometry of a nondegenerate quadratic form (gᵀ Q g = Q) has determinant equal to +1 or -1.

theorem Garrett.isometry_det_sq_eq_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] [NoZeroDivisors R] {Q g : Matrix n n R} (hQ : Q.det ≠ 0) (hiso : g.transpose * Q * g = Q) : g.det ^ 2 = 1

Square of the determinant of a matrix isometry of a nondegenerate quadratic form is 1.