OAI/Algebra/AffineCancellation/Orbit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Orbit polynomials and exponentiation of locally nilpotent derivations.

  1. def OAI.ComplexCancellation.LND.LocallyNilpotent line 14

    Source documentation

    Local nilpotence, allowing the bound zero for the zero element.

    def LocallyNilpotent (D : Derivation k R R) : Prop :=
…
  2. lemma OAI.ComplexCancellation.LND.iterate_zero line 17
  3. lemma OAI.ComplexCancellation.LND.iterate_eq_zero_of_le line 22
  4. lemma OAI.ComplexCancellation.LND.iterate_add line 27
  5. lemma OAI.ComplexCancellation.LND.iterate_smul line 32
  6. lemma OAI.ComplexCancellation.LND.iterate_leibniz line 37
  7. lemma OAI.ComplexCancellation.LND.orbit_support_finite line 60
  8. def OAI.ComplexCancellation.LND.orbit line 70
  9. lemma OAI.ComplexCancellation.LND.orbit_coeff line 75
  10. lemma OAI.ComplexCancellation.LND.orbit_coeff_zero line 79
  11. lemma OAI.ComplexCancellation.LND.orbit_coeff_one line 82
  12. lemma OAI.ComplexCancellation.LND.inv_factorial_choose line 85
  13. lemma OAI.ComplexCancellation.LND.orbit_mul line 93
  14. lemma OAI.ComplexCancellation.LND.orbit_add line 104
  15. lemma OAI.ComplexCancellation.LND.orbit_algebraMap line 109
  16. def OAI.ComplexCancellation.LND.orbitHom line 117
  17. lemma OAI.ComplexCancellation.LND.orbit_injective line 125
  18. lemma OAI.ComplexCancellation.LND.orbit_degree_le_one line 130
  19. lemma OAI.ComplexCancellation.LND.orbit_constant_iff line 136