OAI/Analysis/FreeWords/VariableUltraAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKVariableUltra.coordinateAlgebra line 24
  2. theorem OAI.KKVariableUltra.mem_coordinateAlgebra line 34
  3. instance OAI.KKVariableUltra.coordinateAlgebra_closed line 37
  4. def OAI.KKVariableUltra.coordinateTrace line 58
  5. theorem OAI.KKVariableUltra.coordinateTrace_apply line 70
  6. theorem OAI.KKVariableUltra.coordinateTrace_one line 73
  7. theorem OAI.KKVariableUltra.coordinateTrace_tracial line 76
  8. theorem OAI.KKVariableUltra.gns_norm_sqrt line 81
  9. theorem OAI.KKVariableUltra.coordinate_norm_tendsto line 86