ShiftNilpotence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.derivation_pow_mul_eq_zero line 15
Source documentation
A derivation is locally nilpotent at a product when it is locally nilpotent at each factor. The deliberately loose exponent avoids binomial coefficients.
```
theorem derivation_pow_mul_eq_zero (D : Derivation R A A)
    (m n : ℕ) (a b : A)
    (ha : (D.toLinearMap ^ m) a = 0)
    (hb : (D.toLinearMap ^ n) b = 0) :
    (D.toLinearMap ^ (m + n)) (a * b) = 0 := by
…
```

theorem OAI.Problem346.derivation_exists_pow_add_eq_zero line 50

Source documentation

Pointwise local nilpotence of a derivation is closed under addition.

theorem derivation_exists_pow_add_eq_zero (D : Derivation R A A) (a b : A)
    (ha : ∃ m : ℕ, (D.toLinearMap ^ m) a = 0)
    (hb : ∃ n : ℕ, (D.toLinearMap ^ n) b = 0) :
    ∃ n : ℕ, (D.toLinearMap ^ n) (a + b) = 0 := by
…

theorem OAI.Problem346.derivation_exists_pow_mul_eq_zero line 61

Source documentation

Pointwise local nilpotence of a derivation is closed under multiplication.

theorem derivation_exists_pow_mul_eq_zero (D : Derivation R A A) (a b : A)
    (ha : ∃ m : ℕ, (D.toLinearMap ^ m) a = 0)
    (hb : ∃ n : ℕ, (D.toLinearMap ^ n) b = 0) :
    ∃ n : ℕ, (D.toLinearMap ^ n) (a * b) = 0 := by
…

theorem OAI.Problem346.mvPolynomial_derivation_locally_nilpotent line 78
Source documentation
Local nilpotence on polynomial generators implies local nilpotence everywhere. No finiteness assumption on the variable type is needed, so spectator variables can be retained without changing the argument.
```
theorem mvPolynomial_derivation_locally_nilpotent
    (D : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (hX : ∀ i : σ, ∃ n : ℕ, (D.toLinearMap ^ n) (MvPolynomial.X i) = 0)
    (f : MvPolynomial σ R) : ∃ n : ℕ, (D.toLinearMap ^ n) f = 0 := by
…
```

theorem OAI.Problem346.mvPolynomial_derivation_locally_nilpotent_of_square_zero_X line 93

Source documentation

The square-zero-on-generators criterion used for directional shifts.

theorem mvPolynomial_derivation_locally_nilpotent_of_square_zero_X
    (D : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (hX : ∀ i : σ, D (D (MvPolynomial.X i)) = 0)
    (f : MvPolynomial σ R) : ∃ n : ℕ, (D.toLinearMap ^ n) f = 0 := by
…