OAI/Algebra/AffineCancellation/OrbitRigidity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ComplexCancellation.LND.fixed_of_square_cube line 15

   Source documentation

   Orbit rigidity for a locally nilpotent derivation, with the nonsquare condition in the original coefficient field.

   theorem fixed_of_square_cube (D : Derivation k R R) (hD : LocallyNilpotent D)
       (f : R →ₐ[k] K) (hf : Function.Injective f) {a d u : R}
       (ha : a ≠ 0) (hd : d ≠ 0) (hu : u ≠ 0) (hn : d ^ 2 + a ^ 2 * u ^ 3 ≠ 0)
       (hlin : D (D (d ^ 2 + a ^ 2 * u ^ 3)) = 0)
       (hns : ∀ z : K, z ^ 2 ≠ -(f u) ^ 3) : D a = 0 ∧ D d = 0 ∧ D u = 0 := by
   …

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