OAI/Analysis/Crouzeix/MatrixEndpoint.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Matrix Endpoint.

  1. theorem OAI.CrouzeixHilbert.Endpoint.eq_zero_of_trace_pair_zero line 20
  2. structure OAI.CrouzeixHilbert.Endpoint.MatrixCertificate line 31
  3. theorem OAI.CrouzeixHilbert.Endpoint.exists_matrixCertificate line 46
  4. theorem OAI.CrouzeixHilbert.Endpoint.trace_mul_eq_norm_sqrt_sq line 82
  5. theorem OAI.CrouzeixHilbert.Endpoint.mul_sqrt_eq_zero_of_trace_mul_eq_zero line 97
  6. theorem OAI.CrouzeixHilbert.Endpoint.mul_eq_zero_of_trace_mul_eq_zero line 106
  7. theorem OAI.CrouzeixHilbert.Endpoint.sqrt_mul_eigen line 112
  8. theorem OAI.CrouzeixHilbert.Endpoint.gram_congruence line 128
  9. structure OAI.CrouzeixHilbert.Endpoint.EndpointFactors line 138
  10. theorem OAI.CrouzeixHilbert.Endpoint.exists_endpointFactors line 153
  11. theorem OAI.CrouzeixHilbert.Endpoint.endpointFactors_of_minimum line 239