OAI/Analysis/CharacterCriterion/DetectingSpaces.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.GenericRW.axes line 21
  2. lemma OAI.KirchbergRordam.GenericRW.axes_apply_pivot line 25
  3. lemma OAI.KirchbergRordam.GenericRW.axes_apply_off line 30
  4. lemma OAI.KirchbergRordam.GenericRW.axes_zero line 41
  5. lemma OAI.KirchbergRordam.GenericRW.axes_neg line 45
  6. abbrev OAI.KirchbergRordam.GenericRW.FreeCoordinates line 50
  7. def OAI.KirchbergRordam.GenericRW.freeVector line 52
  8. lemma OAI.KirchbergRordam.GenericRW.freeVector_of_vector line 56
  9. instance OAI.KirchbergRordam.GenericRW.(instance at line 67) line 67
  10. lemma OAI.KirchbergRordam.GenericRW.mulVec_axes line 69
  11. def OAI.KirchbergRordam.GenericRW.kernelChart line 77
  12. lemma OAI.KirchbergRordam.GenericRW.mem_range_kernelChart line 81
  13. lemma OAI.KirchbergRordam.GenericRW.contDiff_freeVector line 92
  14. lemma OAI.KirchbergRordam.GenericRW.contDiff_axes line 102
  15. lemma OAI.KirchbergRordam.GenericRW.contDiff_kernelChart line 113
  16. lemma OAI.KirchbergRordam.GenericRW.card_freeCoordinates line 127
  17. theorem OAI.KirchbergRordam.GenericRW.exists_avoiding_kernels line 136
  18. def OAI.KirchbergRordam.GenericRW.normalizedRow line 175
  19. lemma OAI.KirchbergRordam.GenericRW.normalizedRow_pivot line 179
  20. def OAI.KirchbergRordam.GenericRW.tensorPivot line 184
  21. def OAI.KirchbergRordam.GenericRW.weightedTensorMatrix line 192
  22. lemma OAI.KirchbergRordam.GenericRW.weightedTensorMatrix_pivot line 198
  23. lemma OAI.KirchbergRordam.GenericRW.contDiff_weightedTensorMatrix line 215
  24. theorem OAI.KirchbergRordam.GenericRW.exists_tensor_coordinates line 232
  25. lemma OAI.KirchbergRordam.GenericRW.normalizedRow_eq line 247
  26. def OAI.KirchbergRordam.GenericRW.tensorMatrix line 258
  27. lemma OAI.KirchbergRordam.GenericRW.weightedTensorMatrix_mulVec line 261
  28. theorem OAI.KirchbergRordam.GenericRW.exists_independent_tensor_coordinates line 277
  29. lemma OAI.KirchbergRordam.GenericRW.exists_tensor_exponent line 302
  30. def OAI.KirchbergRordam.GenericRW.tensorBasis line 317
  31. lemma OAI.KirchbergRordam.GenericRW.tensorBasis_map_coordinates line 321
  32. theorem OAI.KirchbergRordam.GenericRW.exists_labels_normalized line 340
  33. theorem OAI.KirchbergRordam.GenericRW.normalize_surjection line 355
  34. theorem OAI.KirchbergRordam.GenericRW.exists_labels_surjective line 387
  35. theorem OAI.KirchbergRordam.GenericRW.exists_plane_quotient line 411
  36. theorem OAI.KirchbergRordam.GenericRW.exists_surjective_postcomposition line 424
  37. theorem OAI.KirchbergRordam.GenericRW.tensor_real_labels line 445
  38. theorem OAI.KirchbergRordam.QuotientNormSupport.distance_eq line 478
  39. theorem OAI.KirchbergRordam.QuotientNormSupport.multiplication_bound line 482
  40. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.quotientNormedRing line 530
  41. def OAI.KirchbergRordam.GenericRW.DetectingSpace.commutatorIdeal line 537
  42. def OAI.KirchbergRordam.GenericRW.DetectingSpace.closedCommutatorIdeal line 540
  43. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.(instance at line 543) line 543
  44. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.(instance at line 551) line 551
  45. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.commutator_mem line 553
  46. abbrev OAI.KirchbergRordam.GenericRW.DetectingSpace.CommutativeQuotient line 557
  47. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.(instance at line 559) line 559
  48. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.quotient_sa_commute line 562
  49. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.quotient_commute line 568
  50. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.(instance at line 577) line 577
  51. instance OAI.KirchbergRordam.GenericRW.DetectingSpace.(instance at line 585) line 585
  52. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.closedCommutatorIdeal_eq_top line 587
  53. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.commutatorIdeal_eq_top line 599
  54. def OAI.KirchbergRordam.GenericRW.DetectingSpace.finiteCommutators line 617
  55. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.finiteCommutators_mono line 620
  56. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.mem_commutatorIdeal_finite line 625
  57. lemma OAI.KirchbergRordam.GenericRW.DetectingSpace.finite_commutators_span_one line 649
  58. theorem OAI.KirchbergRordam.GenericRW.finite_detecting_space line 656