Formal target: Corpus.WikipediaDeterminantalConjecture.determinantal_conjecture
Does the determinant of the sum $A + B$ of two $n \times n$ normal complex matrices $A$ and $B$ always lie in the convex hull of the $n!$ points $\prod\_i (\lambda(A)\_i + \lambda(B)\_{\sigma(i)})$?
Exact formal statement
∀ (n : Type) [inst : Fintype.{0} n] [inst_1 : DecidableEq.{1} n] (d1 d2 : n → Complex)
(U1 U2 : Subtype.{1} fun x => Membership.mem.{0, 0} (unitary.{0} (Matrix.{0, 0, 0} n n Complex)) x),
Membership.mem.{0, 0}
(DFunLike.coe.{1, 1, 1} (convexHull.{0, 0} Real)
(Set.ofPred.{0} fun x =>
Exists.{1} fun σ =>
Eq.{1}
(Finset.prod.{0, 0} Finset.univ.{0} fun i => HAdd.hAdd.{0, 0, 0} (d1 i) (d2 (DFunLike.coe.{1, 1, 1} σ i)))
x))
(Matrix.det.{0, 0}
(HAdd.hAdd.{0, 0, 0}
(HMul.hMul.{0, 0, 0} (HMul.hMul.{0, 0, 0} (Subtype.val.{1} U1) (Matrix.diagonal.{0, 0} d1))
(Subtype.val.{1} (Star.star.{0} U1)))
(HMul.hMul.{0, 0, 0} (HMul.hMul.{0, 0, 0} (Subtype.val.{1} U2) (Matrix.diagonal.{0, 0} d2))
(Subtype.val.{1} (Star.star.{0} U2)))))This target is a formal statement, not a proof of the problem.
Environment availability: available.