BlockInjectivity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.PolynomialShift.eq_zero_of_shift_eq_zero line 18
Source documentation
A polynomial block shift is injective in strictly positive source-minus-destination weight. All other variable blocks are arbitrary spectators.
```
theorem eq_zero_of_shift_eq_zero (src dst : B) (hsd : src ≠ dst)
    {f : MvPolynomial (B × I) ℂ} {p q : ℕ} (hpq : q < p)
    (hp : IsBlockHomogeneous src f p) (hq : IsBlockHomogeneous dst f q)
    (hDf : shift src dst f = 0) : f = 0 := by
…
```
Mentions: OAI.Problem346.PolynomialShift.shift
theorem OAI.Problem346.PolynomialShift.shift_injOn line 43
Source documentation
Injectivity on the intersection of two specified block-homogeneous pieces.
```
theorem shift_injOn (src dst : B) (hsd : src ≠ dst) (p q : ℕ) (hpq : q < p) :
    Set.InjOn (shift (K := ℂ) (I := I) src dst)
…
```
Mentions: OAI.Problem346.PolynomialShift.shift