NYLL
Module

ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
9 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists valuation pow eq valuation zpow of is Algebraic

Imports9
Imported by1

Declarations

theorem

map_natCast_le_one

L39 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.map_natCast_le_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem map_natCast_le_one (n : ℕ) : w n ≤ 1
theorem

map_intCast_le_one

L46 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.map_intCast_le_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem map_intCast_le_one (a : ℤ) : w a ≤ 1
theorem

exists_prime_dvd_map_lt_one

L51 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.exists_prime_dvd_map_lt_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem exists_prime_dvd_map_lt_one {n : ℕ} (hn0 : n ≠ 0) (hn : w n < 1) :
    ∃ p : ℕ, p.Prime ∧ p ∣ n ∧ w p < 1
theorem

map_prime_eq_one_of_ne

L68 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.map_prime_eq_one_of_ne
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem map_prime_eq_one_of_ne {ℓ p : ℕ} (hℓ : ℓ.Prime) (hp : p.Prime) (hwℓ : w ℓ < 1) (hne : p ≠
  ℓ) :
    w p = 1
theorem

map_natCast_eq_one_of_not_dvd

L86 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.map_natCast_eq_one_of_not_dvd
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem map_natCast_eq_one_of_not_dvd {ℓ : ℕ} (hℓ : ℓ.Prime) (hwℓ : w ℓ < 1) {m : ℕ} (hm0 : m ≠ 0)
    (hnd : ¬ ℓ ∣ m) : w m = 1
theorem

exists_map_natCast_eq_pow

L95 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.exists_map_natCast_eq_pow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem exists_map_natCast_eq_pow {ℓ : ℕ} (hℓ : ℓ.Prime) (hwℓ : w ℓ < 1) {n : ℕ} (hn0 : n ≠ 0) :
    ∃ e : ℕ, w n = w ℓ ^ e
theorem

exists_map_eq_zpow

L103 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.exists_map_eq_zpow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem exists_map_eq_zpow {ℓ : ℕ} (hℓ : ℓ.Prime) (hwℓ : w ℓ < 1) {c : ℚ} (hc : c ≠ 0) :
    ∃ k : ℤ, w c = w ℓ ^ k
theorem

exists_prime_map_lt_one

L118 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic.Valuation.RatComm.exists_prime_map_lt_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
namespace Valuation
open _root_.Valuation
namespace RatComm
open _root_.Valuation
variable {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation ℚ Γ₀)
Lean source · statement
theorem exists_prime_map_lt_one {c : ℚ} (hc : c ≠ 0) (h : w c < 1) : ∃ ℓ : ℕ, ℓ.Prime ∧ w ℓ < 1
theorem

exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic

L138 ↗
ValuationSubring.exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
open Valuation.RatComm in
Lean source · statement
theorem _root_.ValuationSubring.exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
    {F : Type*} [Field F] [Algebra ℚ F] [Algebra.IsAlgebraic ℚ F] (O : ValuationSubring F)
    {π₀ : F} (h0 : O.valuation π₀ ≠ 0) (h1 : O.valuation π₀ < 1) {x : F} (hx : x ≠ 0) :
    ∃ m : ℕ, 0 < m ∧ ∃ k : ℤ, O.valuation x ^ m = O.valuation π₀ ^ k

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.