OAI/Analysis/SymmetricDomains/RootMomentCoefficients.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Release061.SignElimination.powerSumPolynomialline 35 - lemma
OAI.Release061.SignElimination.powerSumPolynomial_specline 39 - lemma
OAI.Release061.SignElimination.powerSumPolynomial_evalline 45 - lemma
OAI.Release061.SignElimination.multiset_enumerateline 53 - def
OAI.Release061.SignElimination.rootCoefficientline 65 - lemma
OAI.Release061.SignElimination.roots_esymm_eq_rootCoefficientline 68 - theorem
OAI.Release061.SignElimination.root_moment_coefficientsline 86