Module

ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic

5 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists pow valuation eq valuation nat Cast zpow of is Algebraic

Imports7

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Coprime.Lemmas
Mathlib.Data.Nat.Factorization.Basic
Mathlib.Data.Rat.Cast.Defs
Mathlib.Algebra.CharP.Algebra
Mathlib.Tactic.Conv
Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic

Imported by2

theorem

valuation_intCast_eq_one_of_not_dvd

L37 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic.P2mR1W0zpow.valuation_intCast_eq_one_of_not_dvd

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
namespace P2mR1W0zpow
section ValueGroup
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem valuation_intCast_eq_one_of_not_dvd {p : ℕ} (hp : p.Prime)
    (hAp : A.valuation (p : K) < 1) {a : ℤ} (ha : ¬ (p : ℤ) ∣ a) :
    A.valuation (a : K) = 1

theorem

exists_valuation_natCast_eq_pow

L75 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic.P2mR1W0zpow.exists_valuation_natCast_eq_pow

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
namespace P2mR1W0zpow
section ValueGroup
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem exists_valuation_natCast_eq_pow {p : ℕ} (hp : p.Prime)
    (hAp : A.valuation (p : K) < 1) {n : ℕ} (hn : n ≠ 0) :
    ∃ e : ℕ, A.valuation (n : K) = A.valuation (p : K) ^ e

theorem

exists_valuation_ratCast_eq_zpow

L87 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic.P2mR1W0zpow.exists_valuation_ratCast_eq_zpow

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
namespace P2mR1W0zpow
section ValueGroup
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem exists_valuation_ratCast_eq_zpow [CharZero K] {p : ℕ} (hp : p.Prime)
    (hAp : A.valuation (p : K) < 1) {c : ℚ} (hc : c ≠ 0) :
    ∃ k : ℤ, A.valuation (c : K) = A.valuation (p : K) ^ k

theorem

exists_pow_valuation_eq_valuation_prime_zpow

L107 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic.P2mR1W0zpow.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_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
namespace P2mR1W0zpow
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

theorem

exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic

L121 ↗

ValuationSubring.exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic

Lean source · statement

theorem _root_.ValuationSubring.exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
    {K : Type*} [Field K] [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (A : ValuationSubring K) {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

Module documentation

Valuation Subring exists pow valuation eq valuation nat Cast zpow of is Algebraic

Declarations

valuation_intCast_eq_one_of_not_dvd

exists_valuation_natCast_eq_pow

exists_valuation_ratCast_eq_zpow

exists_pow_valuation_eq_valuation_prime_zpow

exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic