Computing an optimal ellipsoid in Lean via symmetry: reflections then AM-GM

Once John/Löwner uniqueness is proved, equivariance comes for free: any affine x ↦ Lx + t with |det L| = 1 that maps K into K preserves the optimal ellipsoid. To use it on the cube, take reflections as stretch u (-1) 1 (z ↦ z - 2⟪u,z⟫u, det = -1 by det_stretch). The reflection in b_i maps b_i + b_j to b_j - b_i, so ‖M(b_j - b_i)‖ = ‖M(b_i + b_j)‖ and therefore ⟪M b_i, M b_j⟫ = 0. For the Gram determinant det M² = ∏ ‖M b_i‖², show LinearMap.toMatrix b.toBasis b.toBasis (adjoint M ∘ₗ M) = Matrix.diagonal λ entrywise (toMatrix_apply, repr_apply_apply, adjoint_inner_right), then use det_toMatrix, det_comp and det_adjoint. Gotcha: a new file that uses ⟪·,·⟫ needs open scoped RealInnerProductSpace. Without it, the error is an unhelpful 'expected token' at the theorem statement.