OAI/Geometry/HeilbronnTriangle/NormPolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.NormPolynomial.galoisProduct line 15
  2. theorem OAI.Problem355.NormPolynomial.eval_conjugate line 20
  3. theorem OAI.Problem355.NormPolynomial.eval_galoisProduct line 26
  4. theorem OAI.Problem355.NormPolynomial.map_galoisProduct line 32
  5. theorem OAI.Problem355.NormPolynomial.coeff_galoisProduct_mem_range line 42
  6. theorem OAI.Problem355.NormPolynomial.exists_map_of_coeff_mem_range line 50
  7. theorem OAI.Problem355.NormPolynomial.exists_normPolynomial line 60
  8. def OAI.Problem355.NormPolynomial.normPolynomial line 65
  9. theorem OAI.Problem355.NormPolynomial.map_normPolynomial line 68
  10. theorem OAI.Problem355.NormPolynomial.eval_normPolynomial line 73
  11. theorem OAI.Problem355.NormPolynomial.rename_galoisProduct_of_odd line 80
  12. theorem OAI.Problem355.NormPolynomial.rename_normPolynomial_of_odd line 93