rw [hasSliceRankLE_iff]
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE 0 f ↔ f = 0
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (0 = 0 ∧ f = 0 ∨ ∃ n f_1 i g h, HasSliceRankLE n f_1 ∧ 0 = n + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    f = 0