OAI/Analysis/Kaplansky/Regular/ReducedPolynomials.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyConsequences.Regular.Op line 13
  2. def OAI.KaplanskyConsequences.Regular.polynomial line 15
  3. lemma OAI.KaplanskyConsequences.Regular.polynomial_apply line 16
  4. lemma OAI.KaplanskyConsequences.Regular.span_left_mul line 23
  5. lemma OAI.KaplanskyConsequences.Regular.span_left_star line 42
  6. def OAI.KaplanskyConsequences.Regular.polynomialAlgebra line 58
  7. lemma OAI.KaplanskyConsequences.Regular.adjoin_left_le_polynomial line 71
  8. lemma OAI.KaplanskyConsequences.Regular.polynomial_dense line 76
  9. lemma OAI.KaplanskyConsequences.Regular.coefficient_generator line 89
  10. lemma OAI.KaplanskyConsequences.Regular.coefficient_polynomial line 92
  11. lemma OAI.KaplanskyConsequences.Regular.coefficient_norm_le line 99
  12. lemma OAI.KaplanskyConsequences.Regular.polynomial_erase line 107
  13. lemma OAI.KaplanskyConsequences.Regular.polynomial_dense_zero line 116