OAI/Geometry/HeilbronnTriangle/NormEncoding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.NormEncoding.Coordinate line 17
  2. def OAI.Problem355.NormEncoding.monomialExponent line 19
  3. theorem OAI.Problem355.NormEncoding.monomialExponent_injective line 22
  4. theorem OAI.Problem355.NormEncoding.monomialExponent_covers line 27
  5. def OAI.Problem355.NormEncoding.normCoefficient line 41
  6. def OAI.Problem355.NormEncoding.monomialValue line 45
  7. theorem OAI.Problem355.NormEncoding.normCoefficient_swap01 line 48
  8. theorem OAI.Problem355.NormEncoding.normCoefficient_swap12 line 53
  9. theorem OAI.Problem355.NormEncoding.eval_labelNormPolynomial_eq_sum line 58
  10. theorem OAI.Problem355.NormEncoding.two_ne_zero line 69
  11. theorem OAI.Problem355.NormEncoding.eq_zero_of_eq_neg line 75
  12. theorem OAI.Problem355.NormEncoding.normCoefficient_diag01 line 80
  13. theorem OAI.Problem355.NormEncoding.normCoefficient_diag12 line 84
  14. theorem OAI.Problem355.NormEncoding.normCoefficient_diag02 line 88
  15. def OAI.Problem355.NormEncoding.determinantIndexEquiv line 92
  16. def OAI.Problem355.NormEncoding.normRowFunctions line 96
  17. theorem OAI.Problem355.NormEncoding.matrix_of_label_values line 101
  18. theorem OAI.Problem355.NormEncoding.sum_normRowFunctions_eq_eval line 107
  19. theorem OAI.Problem355.NormEncoding.sum_normRowFunctions_ne_zero line 124
  20. theorem OAI.Problem355.NormEncoding.exists_norm_summands line 131