OAI/RepresentationTheory/FoulkesHowe/BackwardCancellation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.eq_zero_of_backward_chain line 8

   Source documentation

   A finite sequence of zero-reflecting transitions can be cancelled backwards.

   theorem eq_zero_of_backward_chain {M : Type*} [Zero M]
       (P : ℕ → M) (m : ℕ)
       (hstep : ∀ k < m, P (k+1) = 0 → P k = 0)
       (hm : P m = 0) : P 0 = 0 := by
   …

2. theorem OAI.Problem346.eq_zero_of_linear_chain line 18

   Source documentation

   Scalar factors in derivative-chain identities need not be divided out when propagating a zero endpoint backwards. Only zero reflection of each derivative on its current polynomial is required.

   theorem eq_zero_of_linear_chain {R M : Type*} [Semiring R]
       [AddCommMonoid M] [Module R M]
       (P : ℕ → M) (D : ℕ → Module.End R M) (c : ℕ → R) (m : ℕ)
       (hchain : ∀ k < m, D k (P k) = c k • P (k+1))
       (hreflect : ∀ k < m, D k (P k) = 0 → P k = 0)
       (hm : P m = 0) : P 0 = 0 := by
   …