𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousConstSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ removeZero p (Nat.succ (Nat.pred n)) = p (Nat.succ (Nat.pred n))
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousConstSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ removeZero p n = p n
rw [← Nat.succ_pred_eq_of_pos h]
no goals
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousConstSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ removeZero p (Nat.succ (Nat.pred n)) = p (Nat.succ (Nat.pred n))
rfl