AlgebraicCurves.Valuations.Proofs.ValuationSubring_mulArchimedean_valueGroup_of_isAlgebraic_of_valuation_natCast_lt_one.P2mR1W0arch.exists_pow_valuation_eq_valuation_prime_zpow
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mulArchimedean_valueGroup_of_isAlgebraic_of_valuation_natCast_lt_one
namespace P2mR1W0arch
section ValueGroup
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]Lean source · statement
theorem exists_pow_valuation_eq_valuation_prime_zpow {p : ℕ} (hp : p.Prime)
(hAp : A.valuation (p : K) < 1) {x : K} (hx : x ≠ 0) :
∃ n : ℕ, 0 < n ∧ ∃ k : ℤ, A.valuation x ^ n = A.valuation (p : K) ^ k