OAI/Analysis/DirectCrouzeix/CompleteBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectCrouzeix.convex_numericalRange line 61
2. theorem OAI.DirectCrouzeix.complete_crouzeix line 65

   Distinct definitions of this name: ComparatorChallenges/DirectCrouzeix.lean:34 (same statement text; different proof or body). Qualify references as OAI.DirectCrouzeix.complete_crouzeix@path.