Theorem: unevenSeries_norm (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ ‖unevenSeries u z1 n‖ = ‖unevenTerm u z1 n‖
Tactic:
rw [unevenSeries, unevenSeries', unevenTerm, ContinuousMultilinearMap.norm_mkPiRing]
State after:
no goals