𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.338474
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ 0 < ⊤
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.338474
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
rw [expSeries_radius_eq_top]
no goals
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.338474
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ 0 < ⊤
exact WithTop.zero_lt_top