Valuations on an algebra over a finite field.

theorem FiniteField.valuation_algebraMap_eq_one {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [Field Fq] [Finite Fq] [Ring A] [Algebra Fq A] [LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq) (ha : a ≠ 0) : v ((algebraMap Fq A) a) = 1

theorem FiniteField.valuation_algebraMap_le_one {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [Field Fq] [Finite Fq] [Ring A] [Algebra Fq A] [LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq) : v ((algebraMap Fq A) a) ≤ 1

instance FiniteField.instIsTrivialOn {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [Field Fq] [Finite Fq] [Ring A] [Algebra Fq A] [LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) : Valuation.IsTrivialOn Fq v