OAI/Algebra/AffineCancellation/Order.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.LND.orbit_ne_zero line 12
2. def OAI.ComplexCancellation.LND.order line 18
3. lemma OAI.ComplexCancellation.LND.order_mul line 21
4. lemma OAI.ComplexCancellation.LND.order_zero_iff line 27
5. lemma OAI.ComplexCancellation.LND.order_derivative line 36
6. lemma OAI.ComplexCancellation.LND.cancel_factor_locallyNilpotent line 47

   Source documentation

   Dividing a locally nilpotent derivation by a nonzero common factor still produces a locally nilpotent derivation, even if the factor is not invariant.

   lemma cancel_factor_locallyNilpotent {S : Type*} [CommRing S] [Algebra k S]
       (f : S →ₐ[k] R) (hf : Function.Injective f)
       (D : Derivation k R R) (hD : LocallyNilpotent D)
       (E : Derivation k S S) {c : R} (hc : c ≠ 0)
       (h : ∀ r : S, D (f r) = c * f (E r)) : LocallyNilpotent E := by
   …

   Mentions: OAI.ComplexCancellation.LND.LocallyNilpotent

7. lemma OAI.ComplexCancellation.LND.cancel_factor_square_zero line 69