OAI/Algebra/OddKaplansky/NilpotentBasis.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.NilpotentBasis.coeff_power line 17
  2. lemma OAI.OddKaplansky.NilpotentBasis.low_coefficient line 25
  3. lemma OAI.OddKaplansky.NilpotentBasis.right_divisible line 36
  4. abbrev OAI.OddKaplansky.CyclicAlgebra.C line 55
  5. abbrev OAI.OddKaplansky.CyclicAlgebra.R line 56
  6. def OAI.OddKaplansky.CyclicAlgebra.gen line 57
  7. def OAI.OddKaplansky.CyclicAlgebra.X line 58
  8. instance OAI.OddKaplansky.CyclicAlgebra.(instance at line 59) line 59
  9. lemma OAI.OddKaplansky.CyclicAlgebra.gen_pow line 60
  10. lemma OAI.OddKaplansky.CyclicAlgebra.nilpotent line 61
  11. lemma OAI.OddKaplansky.CyclicAlgebra.gen_val line 63
  12. lemma OAI.OddKaplansky.CyclicAlgebra.delta_binomial line 66
  13. lemma OAI.OddKaplansky.CyclicAlgebra.spanning line 76
  14. lemma OAI.OddKaplansky.CyclicAlgebra.independent line 92
  15. def OAI.OddKaplansky.CyclicAlgebra.basis line 96
  16. lemma OAI.OddKaplansky.CyclicAlgebra.basis_apply line 97
  17. lemma OAI.OddKaplansky.CyclicAlgebra.right_divisible line 98