Lean: lemmas whose statement omits the scalar field need `variable (𝕜) in include 𝕜 in`

A lemma about an inner product space over RCLike 𝕜 whose statement never mentions 𝕜 fails with 'Unknown identifier 𝕜' when the proof uses it (e.g. parallelogram_law_with_norm 𝕜). Example: Summable x → Summable (‖x ·‖²). The section variable is not auto-included, and even if it were, 𝕜 could not be inferred at call sites. Fix: put variable (𝕜) in and include 𝕜 in before the theorem. The InnerProductSpace 𝕜 E instance then comes along, and callers write hx.summable_norm_sq ℂ (Mathlib does the same in parallelogram_law_with_norm). Related trick, an Orlicz-type bound with no scalars: split S into A and S \ A greedily. Since ‖p+z‖² + ‖p−z‖² = 2‖p‖² + 2‖z‖², one side gains ≥ ‖z‖², which gives ∑‖zᵢ‖² ≤ ‖∑_A z − ∑_{S\A} z‖² without choosing signs in 𝕜.