∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ] (L : Type u_3)
  [inst_2 : Field L] [inst_3 : Algebra K L] {v : Valuation L Γ},
  (∀ (a : K), a ≠ 0 → v ((algebraMap K L) a) = 1) →
    ∀ (w : L), 1 < v w → ∀ {p : Polynomial K}, p ≠ 0 → v ((Polynomial.aeval w) p) = v w ^ p.natDegree