OAI/RepresentationTheory/FoulkesHowe/EncodedCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.multilinearPolynomial_eq_zero_of_replacements line 16

   Source documentation

   Cancel one directional derivative of a repeated-block multilinear polynomial. It suffices that every single source-slot replacement vanishes; no normalization or nonvanishing factorial is needed.

   theorem multilinearPolynomial_eq_zero_of_replacements
       {V S I B : Type*} [AddCommGroup V] [Module ℂ V]
       [Fintype S] [Fintype I] [Fintype B] [hS : DecidableEq S] [hB : DecidableEq B]
       (L : MultilinearMap ℂ (fun _ : S => V) ℂ) (e : I → V)
       (blocks : S → B) (src dst : B) (hsd : src ≠ dst)
       (hdegree : (Finset.univ.filter (fun s => blocks s = dst)).card <
         (Finset.univ.filter (fun s => blocks s = src)).card)
       (hzero : ∀ s, blocks s = src →
         multilinearPolynomial L e (Function.update blocks s dst) = 0) :
       multilinearPolynomial L e blocks = 0 := by
   …

   Mentions: OAI.Problem346.multilinearPolynomial