NYLL
Module

PadicField.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PadicField
26 declarations indexed from sourceView source ↗

Module documentation

The concrete p-adic field ℚ_[p]

This file is the first concrete example leaf for the DVF navigation library. It deliberately uses mathlib's public p-adic objects directly in theorem statements instead of introducing public aliases for ℚ_[p] or its unit group.

Imports4
Imported by14

Declarations

def

padicMulValuationNhds

L38 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicMulValuationNhds
Documentation

The neighbourhood filter on ℚ_[p] induced by Padic.mulValuation. This keeps statements below on the valuation topology instead of the ambient metric topology selected by the global ℚ_[p] instance.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
def padicMulValuationNhds
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p]) : Filter ℚ_[p]
theorem

padicMulValuationNhds_eq_valuedNhds

L45 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicMulValuationNhds_eq_valuedNhds
Documentation

Characterization of the named neighbourhood filter by the topology transported from Padic.mulValuation.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicMulValuationNhds_eq_valuedNhds
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p]) :
    padicMulValuationNhds p x =
      @nhds ℚ_[p] (@UniformSpace.toTopologicalSpace ℚ_[p]
        (Valued.mk' (Padic.mulValuation (p := p))).toUniformSpace) x
abbrev

padicDVRValuation

L55 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation
Documentation

The DVR valuation on ℚ_[p] obtained from the discrete valuation ring ℤ_[p]. This is the chosen-valuation side of the local-field structure theory, the local-field structure classification, for the basic p-adic field.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
abbrev padicDVRValuation (p : ℕ) [Fact p.Prime] :
    _root_.Valuation ℚ_[p] ℤᵐ⁰
def

padicIntEquivValuationSubring

L61 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring
Documentation

The valuation subring of the DVR valuation on ℚ_[p] is the usual p-adic integer ring.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
def padicIntEquivValuationSubring
    (p : ℕ) [Fact p.Prime] :
    ℤ_[p] ≃+* (padicDVRValuation p).valuationSubring
theorem

padicIntEquivValuationSubring_coe

L69 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring_coe
Documentation

The valuation-subring equivalence is the usual inclusion into ℚ_[p] after forgetting the integrality proof.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicIntEquivValuationSubring_coe
    (p : ℕ) [Fact p.Prime] (x : ℤ_[p]) :
    ((padicIntEquivValuationSubring p x :
        (padicDVRValuation p).valuationSubring) : ℚ_[p]) =
      (x : ℚ_[p])
def

padicIntResidueFieldEquivZMod

L77 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntResidueFieldEquivZMod
Documentation

The residue field of ℤ_[p] is ZMod p.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
def padicIntResidueFieldEquivZMod
    (p : ℕ) [Fact p.Prime] :
    IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p
theorem

padicInt_residueField_finite

L83 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicInt_residueField_finite
Documentation

The residue field of ℤ_[p] is finite.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicInt_residueField_finite
    (p : ℕ) [Fact p.Prime] :
    Finite (IsLocalRing.ResidueField ℤ_[p])
instance

padicDVRValuation_isRankOneDiscrete

L90 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_isRankOneDiscrete
Documentation

The valuation in (padicDVRValuation p).IsRankOneDiscrete is rank-one and discrete.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
instance padicDVRValuation_isRankOneDiscrete
    (p : ℕ) [Fact p.Prime] :
    (padicDVRValuation p).IsRankOneDiscrete
theorem

padicDVRValuation_apply_p

L98 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_apply_p
Documentation

The canonical prime element has normalized value exp (-1) for the chosen DVR valuation on ℚ_[p].

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicDVRValuation_apply_p
    (p : ℕ) [Fact p.Prime] :
    padicDVRValuation p (p : ℚ_[p]) =
      WithZero.exp (-1 : ℤ)
theorem

padicDVRValuation_isUniformizer_p

L120 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_isUniformizer_p
Documentation

The canonical prime element is a uniformizer for the chosen DVR valuation on ℚ_[p].

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicDVRValuation_isUniformizer_p
    (p : ℕ) [Fact p.Prime] :
    (padicDVRValuation p).IsUniformizer (p : ℚ_[p])
theorem

padicDVRValuation_isAdicComplete

L130 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_isAdicComplete
Documentation

The valuation subring of the DVR valuation on ℚ_[p] is complete for its maximal-ideal topology. The proof transports mathlib's adic completeness of ℤ_[p] across the explicit valuation-subring equivalence.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicDVRValuation_isAdicComplete
    (p : ℕ) [Fact p.Prime] :
    IsAdicComplete
      (IsLocalRing.maximalIdeal (padicDVRValuation p).valuationSubring)
      (padicDVRValuation p).valuationSubring
instance

padicDVRValuation_isCompleteDiscrete

L203 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_isCompleteDiscrete
Documentation

The standard p-adic valuation is complete as a discrete valuation.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · full declaration
instance padicDVRValuation_isCompleteDiscrete
    (p : ℕ) [Fact p.Prime] :
    Valuation.IsCompleteDiscrete (padicDVRValuation p) where
  isAdicComplete := padicDVRValuation_isAdicComplete p
def

padicCompleteDVF

L209 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF
Documentation

The concrete complete-DVF package for the p-adic field ℚ_[p].

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · full declaration
def padicCompleteDVF
    (p : ℕ) [Fact p.Prime] :
    CompleteDVF ℚ_[p] where
  ValueGroup := ℤᵐ⁰
  valuation := padicDVRValuation p
  instCompleteDiscrete := inferInstance
theorem

padicCompleteDVF_residueField_finite

L217 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF_residueField_finite
Documentation

The residue field of the complete-DVF package on ℚ_[p] is finite.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicCompleteDVF_residueField_finite
    (p : ℕ) [Fact p.Prime] :
    Finite (padicCompleteDVF p).residueField
theorem

padicCompleteDVF_residueField_card

L234 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF_residueField_card
Documentation

The residue field of the concrete complete-DVF package on ℚ_[p] has cardinality exactly p.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padicCompleteDVF_residueField_card
    (p : ℕ) [Fact p.Prime] :
    Nat.card (padicCompleteDVF p).residueField = p
def

padicLocalField

L261 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicLocalField
Documentation

The local-field structure theory, the local-field structure classification, p-adic base-field direction: ℚ_[p] is a local field in the chosen-complete-DVF sense used in this formalization.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
def padicLocalField
    (p : ℕ) [Fact p.Prime] :
    LocalField ℚ_[p]
theorem

padic_mulValuation_natCast_of_ne_zero

L271 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padic_mulValuation_natCast_of_ne_zero
Documentation

mathlib's bundled p-adic multiplicative valuation has the expected value on nonzero natural-number denominators.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padic_mulValuation_natCast_of_ne_zero
    (p n : ℕ) [Fact p.Prime] (hn : n ≠ 0) :
    Padic.mulValuation (p := p) ((n : ℕ) : ℚ_[p]) =
      WithZero.exp (-(padicValNat p n : ℤ))
theorem

padic_mulValuation_logSeries_denominator

L281 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padic_mulValuation_logSeries_denominator
Documentation

Successor form of the natural-number denominator valuation used in the logarithm-series estimate.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padic_mulValuation_logSeries_denominator
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Padic.mulValuation (p := p) ((n + 1 : ℕ) : ℚ_[p]) =
      WithZero.exp (-(padicValNat p (n + 1) : ℤ))
theorem

padic_mulValuation_expSeries_denominator

L290 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padic_mulValuation_expSeries_denominator
Documentation

Factorial-denominator form used by the exponential-series estimate.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem padic_mulValuation_expSeries_denominator
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Padic.mulValuation (p := p) ((n.factorial : ℕ) : ℚ_[p]) =
      WithZero.exp (-(padicValNat p n.factorial : ℤ))
theorem

tendsto_zero_logSeriesTermField_padic_mulValuation_of_lt_one

L301 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.tendsto_zero_logSeriesTermField_padic_mulValuation_of_lt_one
Documentation

Standard p-adic specialization of the logarithm-term convergence estimate: if v x < 1 for mathlib's Padic.mulValuation, then the unsigned logarithm-series terms tend to zero.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · full declaration
theorem tendsto_zero_logSeriesTermField_padic_mulValuation_of_lt_one
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p])
    (hvx : Padic.mulValuation (p := p) x <
      (1 : WithZero (Multiplicative ℤ))) :
    Tendsto
      (fun n : ℕ =>
        MultiplicativeIntegerValuation.logSeriesTermField x
          (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n)) n)
      atTop (padicMulValuationNhds p (0 : ℚ_[p])) := by
  rw [padicMulValuationNhds_eq_valuedNhds]
  exact
    MultiplicativeIntegerValuation.tendsto_zero_logSeriesTermField_ofWithZeroValuation_of_lt_one
      (v := Padic.mulValuation (p := p)) (p := p) x
      (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n))
      (padic_mulValuation_logSeries_denominator p) hvx
theorem

tendsto_zero_signedLogSeriesTermField_padic_mulValuation_of_lt_one

L322 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.tendsto_zero_signedLogSeriesTermField_padic_mulValuation_of_lt_one
Documentation

Signed version of tendsto_zero_logSeriesTermField_padic_mulValuation_of_lt_one.

Source context 10 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation (
  tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
) in
Lean source · full declaration
theorem tendsto_zero_signedLogSeriesTermField_padic_mulValuation_of_lt_one
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p])
    (hvx : Padic.mulValuation (p := p) x <
      (1 : WithZero (Multiplicative ℤ))) :
    Tendsto
      (fun n : ℕ =>
        MultiplicativeIntegerValuation.signedLogSeriesTermField x
          (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n)) n)
      atTop (padicMulValuationNhds p (0 : ℚ_[p])) := by
  rw [padicMulValuationNhds_eq_valuedNhds]
  exact
    tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
      (v := Padic.mulValuation (p := p)) (p := p) x
      (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n))
      (padic_mulValuation_logSeries_denominator p) hvx
theorem

tendsto_zero_expSeriesTermField_padic_mulValuation_of_lt_exp_neg_one

L343 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.tendsto_zero_expSeriesTermField_padic_mulValuation_of_lt_exp_neg_one
Documentation

Standard p-adic specialization of the exponential-term convergence estimate on the radius v x < exp (-1).

Source context 10 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation (
  tendsto_zero_expSeriesTermField_ofWithZeroValuation_of_lt_exp_neg_one
) in
Lean source · full declaration
theorem tendsto_zero_expSeriesTermField_padic_mulValuation_of_lt_exp_neg_one
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p])
    (hvx : Padic.mulValuation (p := p) x < WithZero.exp (-1 : ℤ)) :
    Tendsto
      (fun n : ℕ =>
        MultiplicativeIntegerValuation.expSeriesTermField x
          (fun n => Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)) n)
      atTop (padicMulValuationNhds p (0 : ℚ_[p])) := by
  rw [padicMulValuationNhds_eq_valuedNhds]
  exact
    tendsto_zero_expSeriesTermField_ofWithZeroValuation_of_lt_exp_neg_one
      (v := Padic.mulValuation (p := p)) (p := p) x
      (fun n => Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n))
      (padic_mulValuation_expSeries_denominator p) hvx
theorem

mem_rootsOfUnity_padic_iff

L360 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.mem_rootsOfUnity_padic_iff
Documentation

Membership in mathlib's p^m-power roots of unity inside the actual p-adic unit group is the usual unit equation.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem mem_rootsOfUnity_padic_iff
    (p m : ℕ) [Fact p.Prime] (ζ : (ℚ_[p])ˣ) :
    ζ ∈ rootsOfUnity (p ^ m) ℚ_[p] ↔ ζ ^ (p ^ m) = 1
theorem

mem_rootsOfUnity_padic_iff_coe_pow

L367 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.mem_rootsOfUnity_padic_iff_coe_pow
Documentation

The same roots-of-unity criterion after coercing the p-adic unit to ℚ_[p].

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem mem_rootsOfUnity_padic_iff_coe_pow
    (p m : ℕ) [Fact p.Prime] (ζ : (ℚ_[p])ˣ) :
    ζ ∈ rootsOfUnity (p ^ m) ℚ_[p] ↔
      ((ζ : ℚ_[p]) ^ (p ^ m) = 1)
theorem

one_mem_rootsOfUnity_padic

L375 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.one_mem_rootsOfUnity_padic
Documentation

The identity p-adic unit lies in every finite p-power roots-of-unity subgroup.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem one_mem_rootsOfUnity_padic
    (p m : ℕ) [Fact p.Prime] :
    (1 : (ℚ_[p])ˣ) ∈ rootsOfUnity (p ^ m) ℚ_[p]
theorem

primitiveRoot_isRoot_cyclotomic_padic

L382 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.primitiveRoot_isRoot_cyclotomic_padic
Documentation

A primitive p-adic p^m-power root is a root of mathlib's corresponding cyclotomic polynomial over ℚ_[p].

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
namespace Examples
namespace Qp
open Filter
open scoped Topology
open scoped WithZero
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem primitiveRoot_isRoot_cyclotomic_padic
    (p m : ℕ) [Fact p.Prime] {ζ : ℚ_[p]}
    (hζ : IsPrimitiveRoot ζ (p ^ m)) :
    (Polynomial.cyclotomic (p ^ m) ℚ_[p]).IsRoot ζ

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