OAI/RepresentationTheory/FoulkesHowe/DerivationInjectivity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.derivation_eq_zero_of_positive_weight line 16

   Source documentation

   An algebraic form of the positive-weight injectivity criterion for polynomial derivations. The generator condition admits arbitrary spectator variables.

   theorem derivation_eq_zero_of_positive_weight
       (D E H : Derivation K (MvPolynomial σ K) (MvPolynomial σ K))
       (hED : ⁅E, D⁆ = H) (hHE : ⁅H, E⁆ = (2 : K) • E)
       (hEX : ∀ i : σ, E (E (X i)) = 0)
       (f : MvPolynomial σ K) (p q : ℕ) (hpq : q < p)
       (hf : H f = ((p : K) - q) • f) (hDf : D f = 0) : f = 0 := by
   …