OAI/RepresentationTheory/SpinAngle/TypeAngle.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SpinAngle.TypeAngle.row line 35

    Also declared: ComparatorChallenges/SpinAngle.lean:511 (same declaration text).

  2. def OAI.SpinAngle.TypeAngle.column line 36

    Also declared: ComparatorChallenges/SpinAngle.lean:513 (same declaration text).

  3. def OAI.SpinAngle.TypeAngle.phi line 38

    Also declared: ComparatorChallenges/SpinAngle.lean:515 (same declaration text).

  4. def OAI.SpinAngle.TypeAngle.columnRoot line 41
  5. def OAI.SpinAngle.TypeAngle.meanRoot line 43
  6. def OAI.SpinAngle.TypeAngle.meanInvRoot line 45
  7. def OAI.SpinAngle.TypeAngle.meanSupport line 47
  8. def OAI.SpinAngle.TypeAngle.rowRoot line 49
  9. lemma OAI.SpinAngle.TypeAngle.columnRoot_support line 52
  10. lemma OAI.SpinAngle.TypeAngle.meanRoot_eq line 63
  11. lemma OAI.SpinAngle.TypeAngle.meanRoot_commute_global line 69
  12. lemma OAI.SpinAngle.TypeAngle.meanRoot_commute_rows line 75
  13. lemma OAI.SpinAngle.TypeAngle.global_norm line 81
  14. lemma OAI.SpinAngle.TypeAngle.cell_norm line 93
  15. theorem OAI.SpinAngle.TypeAngle.nonempty_columns line 105
  16. lemma OAI.SpinAngle.TypeBlocks.dimension_pos line 164
  17. lemma OAI.SpinAngle.TypeBlocks.dimension_le line 167
  18. theorem OAI.SpinAngle.TypeAngle.one_sided_type_angle line 189

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:518 (different declaration text). Qualify references as OAI.SpinAngle.TypeAngle.one_sided_type_angle@path.