Lean: polar of a linear preimage via dotProduct_mulVec + vecMul_transpose

To show polar (toLin' M ⁻¹' K) = toLin' (M⁻¹)ᵀ ⁻¹' polar K on Fin n → ℝ, where polar K = {y | ∀ x ∈ K, ∑ i, x i * y i ≤ 1}, prove the key identity ∑ xᵢyᵢ = ∑ (M *ᵥ x)ᵢ ((M⁻¹)ᵀ *ᵥ y)ᵢ like this: change x ⬝ᵥ y = (M *ᵥ x) ⬝ᵥ ((M⁻¹)ᵀ *ᵥ y), then rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec, nonsing_inv_mul _ hM, one_mulVec] with hM : IsUnit M.det. That closes it; no dotProduct_comm is needed. Get the volume factor from Measure.map_apply + Real.map_matrix_volume_pi_eq_smul_volume_pi (factor ofReal |det M|⁻¹). Get det of (M⁻¹)ᵀ from det_transpose, det_nonsing_inv, Ring.inverse_eq_inv'. Writing linear images as preimages avoids image-measurability issues entirely.