OAI/LinearAlgebra/Hadamard/CubeFibers.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Cubic values, their multiplicities, and cancellation on each fibre.

  1. def OAI.HadamardSix.cubeFiber line 11

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:21 (same declaration text).

  2. lemma OAI.HadamardSix.mem_cubeFiber line 15
  3. lemma OAI.HadamardSix.sum_cubes_of_two_values line 20
  4. lemma OAI.HadamardSix.cubeFiber_card_three line 41
  5. lemma OAI.HadamardSix.ratio_cube_multiplicities line 50
  6. lemma OAI.HadamardSix.ratio_cubeFiber_sum_zero line 72
  7. def OAI.HadamardSix.rowRatio line 96

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:25 (same declaration text).

  8. lemma OAI.HadamardSix.rowRatio_norm line 99
  9. lemma OAI.HadamardSix.rowRatio_first_sum line 102
  10. lemma OAI.HadamardSix.rowRatio_second_sum line 106
  11. lemma OAI.HadamardSix.rowRatio_polynomial line 111
  12. lemma OAI.HadamardSix.rowRatio_cube_multiplicities line 119
  13. def OAI.HadamardSix.IsDephased line 129
  14. lemma OAI.HadamardSix.dephase_isDephased line 131
  15. lemma OAI.HadamardSix.dephased_row_cube_multiplicities line 134
  16. lemma OAI.HadamardSix.dephased_column_cube_multiplicities line 149
  17. lemma OAI.HadamardSix.dephased_row_cube_support line 158
  18. lemma OAI.HadamardSix.rowRatio_cubeFiber_sum_zero line 172

    Distinct definitions of this name: ComparatorChallenges/HadamardCubeFiber.lean:28 (same statement text; different proof or body). Qualify references as OAI.HadamardSix.rowRatio_cubeFiber_sum_zero@path.