OAI/Analysis/NumericalRange/TestingAlgebra.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CompleteCrouzeix.tensorTesting_starline 13 - lemma
OAI.CompleteCrouzeix.tensorTesting_similarityline 23 - def
OAI.CompleteCrouzeix.hermitianFieldline 68 - lemma
OAI.CompleteCrouzeix.hermitianField_hermitianline 70 - lemma
OAI.CompleteCrouzeix.hermitianField_integralline 76 - lemma
OAI.CompleteCrouzeix.densityField_testing_sumline 95 - lemma
OAI.CompleteCrouzeix.matrixFourierTrace_starline 103 - lemma
OAI.CompleteCrouzeix.hsTrace_matrixFourier_starline 111