∀ {Γ₀ : Type u_1} [inst : LinearOrderedCommMonoidWithZero Γ₀] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ₀)
  {Fq : Type u_3} [inst_2 : Field Fq] [Finite Fq] [inst_4 : Algebra Fq A] (a : Fq), ¬a = 0 → v ((algebraMap Fq A) a) ≤ 1