OAI/RepresentationTheory/FoulkesHowe/GridCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.zero_of_upward_grid line 11

   Source documentation

   Reverse induction over a finite rectangular grid. A zero at its upper corner propagates to every point when a one-coordinate upward step can be cancelled.

   theorem zero_of_upward_grid {ι M : Type*} [Fintype ι] [DecidableEq ι] [Zero M]
       (r : ℕ) (F : (ι → ℕ) → M)
       (hend : F (fun _ => r) = 0)
       (hstep : ∀ (c : ι → ℕ), (∀ i, c i ≤ r) → ∀ i, c i < r →
         F (Function.update c i (c i + 1)) = 0 → F c = 0)
       (c : ι → ℕ) (hc : ∀ i, c i ≤ r) : F c = 0 := by
   …