@[deprecated FiniteField.valuation_algebraMap_eq_one (since := "2026-03-31")]

theorem Valuation.FiniteField.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

Alias of FiniteField.valuation_algebraMap_eq_one.

@[deprecated FiniteField.valuation_algebraMap_le_one (since := "2026-03-31")]

theorem Valuation.FiniteField.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

Alias of FiniteField.valuation_algebraMap_le_one.

@[deprecated FiniteField.instIsTrivialOn (since := "2026-03-31")]

theorem Valuation.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 Γ) : IsTrivialOn Fq v

Alias of FiniteField.instIsTrivialOn.