BinomialVanishing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExternalTensor.Binomial.isZero_biproduct_iff line 11
Source documentation
A finite biproduct is zero exactly when all its summands are zero.
```
theorem isZero_biproduct_iff [HasFiniteBiproducts C] {I : Type} [Fintype I] (f : I → C) :
    IsZero (⨁ f) ↔ ∀ i, IsZero (f i) := by
…
```
theorem OAI.ExternalTensor.Binomial.isZero_shift_iff line 25
Source documentation
Integer shifts preserve and reflect the zero object.
```
theorem isZero_shift_iff (X : C) (n : ℤ) : IsZero (X⟦n⟧) ↔ IsZero X := by
…
```
theorem OAI.ExternalTensor.Binomial.binomialObject_isZero_iff line 35
Source documentation
The q=0 summand always occurs once, so the binomial expansion detects zero.
```
theorem binomialObject_isZero_iff (b d : ℤ) (j : ℕ) (X : C) :
    IsZero (binomialObject b d j X) ↔ IsZero X := by
…
```
Mentions: OAI.ExternalTensor.Binomial.binomialObject

theorem OAI.ExternalTensor.Binomial.iteration_isZero_iff line 51

Source documentation

Exact zero detection for the iterates; no faithfulness of M is silently assumed.

theorem iteration_isZero_iff
    (split : ∀ Y, Phi.obj (M Y) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+d⟧)
    (j : ℕ) (Y : S) :
    IsZero ((Phi.obj^[j]) (M Y)) ↔ IsZero (M ((H^[j]) Y)) :=
…

theorem OAI.ExternalTensor.Binomial.iteration_nonzero_iff line 58