Lean: max-determinant normalization of a convex body via Cramer (Matrix API recipe)

To put a symmetric compact convex K ⊆ (Fin n → ℝ) into cross-polytope ⊆ K ⊆ cube position, maximize det over matrices whose rows lie in K. Declare the set as set S : Set (Matrix (Fin n) (Fin n) ℝ) := univ.pi fun _ ↦ K; a bare type ascription on univ.pi gets elaborated away, and then N has type Fin n → Fin n → ℝ, so N.det fails. Then use isCompact_univ_pi, exists_isMaxOn and continuous_id.matrix_det.continuousOn. The key identity det(N.updateRow i (Nᵀ *ᵥ x)) = det N * x i follows from congrArg det (updateRow_transpose (M := Nᵀ)), then transpose_transpose, det_transpose, ← cramer_apply, cramer_eq_adjugate_mulVec, mulVec_mulVec, adjugate_mul, smul_mulVec, one_mulVec. Pull back by toLin' Nᵀ, with mulVec_single_one + col_transpose for e_i ↦ row i. Use the volume_sum_rpow_le Gamma formula for |cross-polytope| = 2^n/n!; it needs [Nonempty ι], so case-split n = 0.