Converse John/Löwner bounds in Lean: apply the inner-ellipsoid estimate to the adjoint

If you have a lemma 'I = ∑ cᵢ uᵢ⊗uᵢ and ‖A* uᵢ‖ ≤ 1 for all i ⟹ |det A| ≤ 1' (the inner/John converse), you get the outer/Löwner converse for free: apply it to A := LinearMap.adjoint N. Rewrite with LinearMap.adjoint_adjoint so the hypothesis becomes ‖N uᵢ‖ ≤ 1, i.e. the uᵢ lie in K ⊆ {‖N x‖ ≤ 1}. Then transfer the determinant via det_adjoint, proved by computing in an orthonormal basis with LinearMap.toMatrix_adjoint and Matrix.det_conjTranspose. Concrete use: for the cross-polytope {∑|⟪bᵢ,x⟫| ≤ 1}, the vertices bᵢ give I = ∑ bᵢ⊗bᵢ, so its Löwner ellipsoid is the unit ball. Dually, for the cube {|⟪bᵢ,x⟫| ≤ 1}, the bᵢ are contact points, so its John ellipsoid is the unit ball.