OAI/LinearAlgebra/Hadamard/Polynomials.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernel identities and symmetric polynomials of row ratios.

  1. lemma OAI.HadamardSix.character_sub line 11
  2. lemma OAI.HadamardSix.column_kernel_identity line 15
  3. lemma OAI.HadamardSix.same_matrix_identity line 46
  4. def OAI.HadamardSix.elementary line 80
  5. lemma OAI.HadamardSix.elementary_eq_sum line 83
  6. lemma OAI.HadamardSix.elementary_zero line 87
  7. lemma OAI.HadamardSix.elementary_one line 90
  8. lemma OAI.HadamardSix.elementary_six line 93
  9. lemma OAI.HadamardSix.elementary_two_of_power_sums line 100
  10. lemma OAI.HadamardSix.elementary_complement line 113
  11. def OAI.HadamardSix.ratioPolynomial line 133
  12. lemma OAI.HadamardSix.ratioPolynomial_vieta line 136
  13. lemma OAI.HadamardSix.ratioPolynomial_of_power_sums line 145
  14. lemma OAI.HadamardSix.ratioPolynomial_eval line 159
  15. lemma OAI.HadamardSix.ratio_power_six line 166
  16. lemma OAI.HadamardSix.ratio_cubes_two_values line 173
  17. lemma OAI.HadamardSix.three_mul_elementary_three line 180
  18. lemma OAI.HadamardSix.fourth_power_sum_zero line 193