theorem scaling_lemma {K : Type u_1} [Field K] (A : ValuationSubring K) (n : ℕ) (x : Fin (n + 1) → K) (hx : ∀ (i : Fin (n + 1)), x i ≠ 0) : ∃ (l : K) (_ : l ≠ 0) (hmem : ∀ (i : Fin (n + 1)), l * x i ∈ A) (i : Fin (n + 1)), IsUnit ⟨l * x i, ⋯⟩

Scaling Lemma (Lemma 16.32). Given finitely many nonzero elements $x_0, \ldots, x_n \in K$ of a field equipped with a valuation subring $A$, there exists a nonzero scalar $\lambda \in K$ such that all $\lambda x_i$ lie in $A$ and at least one $\lambda x_i$ is a unit of $A$.