Determinant of an element of orthogonal/unitary groups

Stream: maths

[Heather Macbeth]

Since #7635 (@Anne Baanen) it is possible to state that the determinant of an isometry has absolute value 1:

import analysis.normed_space.inner_product
import linear_algebra.determinant

variables (𝕜 : Type*) [is_R_or_C 𝕜]
variables {E : Type*} [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E]

open is_R_or_C

lemma linear_isometry.abs_det (f : E →ₗᵢ[𝕜] E) : abs f.to_linear_map.det = 1 := sorry

Is this on someone's to-do list? How should it even be proved? (Since mathlib doesn't have the adjoint construction ... the conjugate linear map problem again.)