OAI/Analysis/Kaplansky/Regular/RegularOperators.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KaplanskyConsequences.Regular.diagonal_apply line 16
  2. lemma OAI.KaplanskyConsequences.Regular.diagonal_norm_le line 19
  3. lemma OAI.KaplanskyConsequences.Regular.diagonal_one line 22
  4. lemma OAI.KaplanskyConsequences.Regular.diagonal_mul line 24
  5. lemma OAI.KaplanskyConsequences.Regular.diagonal_star line 27
  6. def OAI.KaplanskyConsequences.Regular.diagonalHom line 34
  7. lemma OAI.KaplanskyConsequences.Regular.diagonal_left_commute line 44
  8. def OAI.KaplanskyConsequences.Regular.mask line 47
  9. lemma OAI.KaplanskyConsequences.Regular.mask_apply line 54
  10. lemma OAI.KaplanskyConsequences.Regular.mask_norm_le line 59
  11. lemma OAI.KaplanskyConsequences.Regular.mask_star line 62
  12. lemma OAI.KaplanskyConsequences.Regular.mask_sq line 70
  13. lemma OAI.KaplanskyConsequences.Regular.diagonal_mask_commute line 75
  14. def OAI.KaplanskyConsequences.Regular.negative line 82
  15. def OAI.KaplanskyConsequences.Regular.creation line 85
  16. def OAI.KaplanskyConsequences.Regular.annihilation line 87
  17. lemma OAI.KaplanskyConsequences.Regular.left_split line 90
  18. lemma OAI.KaplanskyConsequences.Regular.creation_apply line 94
  19. lemma OAI.KaplanskyConsequences.Regular.creation_support line 103
  20. lemma OAI.KaplanskyConsequences.Regular.creation_orthogonal line 109
  21. lemma OAI.KaplanskyConsequences.Regular.creation_star_mul_self line 127
  22. lemma OAI.KaplanskyConsequences.Regular.annihilation_star_mul_self line 139