OAI/NumberTheory/Ostmann/Arithmetic/PolynomialFlagReplacementFiniteReindex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.divisibilityIndicator line 11
  2. def OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.flagError line 14
  3. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.zero_polynomial_flag line 18
  4. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.zero_polynomial_error line 22
  5. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.flagError_nonneg line 25
  6. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.totalDegree_rename_equiv line 28
  7. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.rename_ne_zero line 31
  8. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.eval_rename_equiv line 35
  9. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.divisibilityIndicator_rename_equiv line 38
  10. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.flagError_rename_equiv line 43
  11. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.fin_flagError_eq line 52
  12. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.product_sum_reindex line 64
  13. theorem OAI.Ostmann.Arithmetic.PolynomialFlagReplacementFinite.expectation_reindex_eq_product_sum line 88