Valuations on algebras over finite fields

Basic results on valuations over Fq-algebras.

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

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

@[instance 100]

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