This is the volume factor of a linear map

I have encountered the expression sqrt(det(T' * T)) a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it.

Zulip thread #Is there code for X? > (norm of) "determinant" of map between inner product spaces

One motivation to define this is to state volume formula under transformations. From Measure theory and fine properties of functions:

• Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$. This is proved in this PR at euclideanHausdorffMeasure_image_eq_normDet_mul_volume
• Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f^{-1}{y}) d\mathcal{H}^n(y)$, where $J f$ is the normDet of the rectangular Jacobian matrix

AI usage disclosure: AI was used in the following parts

• searching for related literature for an appropriate name
• generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me.

• depends on: [Merged by Bors] - feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent #37918