Module

PadicInt_natCard_quotient_range_eq_pow_valuation_det.lean

Nyll.AlgebraicCurves.Valuations.PadicInt_natCard_quotient_range_eq_pow_valuation_det

5 declarations indexed from sourceView source ↗

Module documentation

Padic Int nat Card quotient range eq pow valuation det

Imports12

Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Data.ZMod.Basic
Mathlib.LinearAlgebra.Determinant
Mathlib.LinearAlgebra.FreeModule.PID
Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Mathlib.NumberTheory.Padics.PadicIntegers
Mathlib.NumberTheory.Padics.RingHoms
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Tactic.ByContra
Mathlib.Tactic.Ext

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

valuation_units

L40 ↗

AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det.ProofAuxSnf716.valuation_units

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det
namespace ProofAuxSnf716
open Module Submodule
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem valuation_units (u : ℤ_[p]ˣ) : (u : ℤ_[p]).valuation = 0

theorem

valuation_prod

L45 ↗

AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det.ProofAuxSnf716.valuation_prod

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det
namespace ProofAuxSnf716
open Module Submodule
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem valuation_prod {ι : Type*} (s : Finset ι) (a : ι → ℤ_[p]) (ha : ∀ i ∈ s, a i ≠ 0) :
    (∏ i ∈ s, a i).valuation = ∑ i ∈ s, (a i).valuation

theorem

natCard_quotient_span_singleton

L56 ↗

AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det.ProofAuxSnf716.natCard_quotient_span_singleton

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det
namespace ProofAuxSnf716
open Module Submodule
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem natCard_quotient_span_singleton (a : ℤ_[p]) (ha : a ≠ 0) :
    Nat.card (ℤ_[p] ⧸ Ideal.span ({a} : Set ℤ_[p])) = p ^ a.valuation

theorem

main

L68 ↗

AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det.ProofAuxSnf716.main

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det
namespace ProofAuxSnf716
open Module Submodule
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem main (p : ℕ) [Fact p.Prime]
    {T : Type*} [AddCommGroup T] [Module ℤ_[p] T] [Module.Free ℤ_[p] T] [Module.Finite ℤ_[p] T]
    (f : Module.End ℤ_[p] T) (hf : LinearMap.det f ≠ 0) :
    Nat.card (T ⧸ LinearMap.range f) = p ^ (LinearMap.det f).valuation

theorem

natCard_quotient_range_eq_pow_valuation_det

L121 ↗

PadicInt.natCard_quotient_range_eq_pow_valuation_det

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.PadicInt_natCard_quotient_range_eq_pow_valuation_det

Lean source · statement

theorem _root_.PadicInt.natCard_quotient_range_eq_pow_valuation_det (p : ℕ) [Fact p.Prime]
    {T : Type*} [AddCommGroup T] [Module ℤ_[p] T] [Module.Free ℤ_[p] T] [Module.Finite ℤ_[p] T]
    (f : Module.End ℤ_[p] T) (hf : LinearMap.det f ≠ 0) :
    Nat.card (T ⧸ LinearMap.range f) = p ^ (LinearMap.det f).valuation

Module documentation

Padic Int nat Card quotient range eq pow valuation det

Declarations

valuation_units

valuation_prod

natCard_quotient_span_singleton

main

natCard_quotient_range_eq_pow_valuation_det