Lean: volume of an explicit simplex polar via matrix determinant lemma + affine preimage

To compute |(Δ−c)°| for the corner simplex, first show the polar equals {z | −m ≤ 1 ∧ ∀ i, z_i − m ≤ 1} with m = (∑z)/(n+1): ⟪x−c, z⟫ = ∑ x_i (z_i − m) + (1 − ∑x)(−m) is a convex combination. Then write it as toLin' A ⁻¹' ((fun w ↦ v − w) ⁻¹' Δ). Use Measure.measurePreserving_sub_left volume v for the outer map and Real.map_matrix_volume_pi_eq_smul_volume_pi for the linear part. For det(I − aJ), set M := (1 : Matrix (Fin n) (Fin n) ℝ) + replicateCol Unit (fun _ : Fin n ↦ -a) * replicateRow Unit (fun _ : Fin n ↦ 1). Ascribe the function domains, or Lean infers Matrix Unit Unit and the HAdd instance fails. Then apply Matrix.det_one_add_replicateCol_mul_replicateRow, which needs an explicit import Mathlib.LinearAlgebra.Matrix.SchurComplement. Do the membership algebra in terms of S = ∑z and a with the fact n·a = 1 − a; linear_combination (a*S) * hna closes the sum identity.