OAI/Algebra/AffineCancellation/Primitive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.LND.iterate_replica line 11
2. lemma OAI.ComplexCancellation.LND.replica line 23
3. lemma OAI.ComplexCancellation.LND.primitive_of_order line 31

   Source documentation

   Remove all common powers of a regular parameter from an LND. The termination certificate is the exact finite order of a single nonzero image.

   lemma primitive_of_order (q : R) (hq : q ≠ 0) (w b s : R) (hs : ¬q ∣ s)
       (n : ℕ) (D : Derivation k R R) (hD : LocallyNilpotent D)
       (hDq : D q=0) (hDw : D w=0) (hb : D b=q^n*s) :
       ∃ E : Derivation k R R, LocallyNilpotent E ∧ E q=0 ∧ E w=0 ∧ ∃ r, ¬q ∣ E r := by
   …

   Mentions: OAI.ComplexCancellation.s, OAI.ComplexCancellation.LND.LocallyNilpotent