English
There exist C>0 with ‖p_n‖ ≤ C for all n when r is below the radius in the uniform sense.
Русский
Существуют C>0 такие, что ‖p_n‖ ≤ C для всех n при r ниже радиуса (однородно).
LaTeX
$$$\\exists C>0:\\forall n,\\|p_n\\| ≤ C.$$$
Lean4
/-- The right inverse does not depend on the zeroth coefficient of a formal multilinear
series. -/
theorem rightInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
p.removeZero.rightInv i x = p.rightInv i x := by
ext1 n
induction n using Nat.strongRec' with
| _ n IH
match n with
| 0 => simp only [rightInv_coeff_zero]
| 1 => simp only [rightInv_coeff_one]
| n + 2 =>
simp only [rightInv, neg_inj]
rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
congr (config := { closePost := false }) 2 with k
by_cases hk : k < n + 2 <;> simp [hk, IH]
