OAI/Analysis/Crouzeix/Vectorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Vectorization.

  1. def OAI.CrouzeixHilbert.vectorization line 18
  2. theorem OAI.CrouzeixHilbert.vectorization_coordinates line 22
  3. theorem OAI.CrouzeixHilbert.norm_vectorization line 31
  4. theorem OAI.CrouzeixHilbert.kronecker_toHS line 35
  5. theorem OAI.CrouzeixHilbert.tensorOperator_vectorization line 50
  6. theorem OAI.CrouzeixHilbert.Endpoint.EndpointFactors.exists_colligation line 65