NYLL
Module

SUnitPowerQuotient.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.SUnitPowerQuotient
27 declarations indexed from sourceView source ↗

Module documentation

Power quotients of S-unit groups

The finite n-th-power quotient of an S-unit group, its cardinality, and explicit ZMod n coordinates.

Imports4
Imported by7

Declarations

def

totalPlaceCard

L33 ↗
KummerTheory.totalPlaceCard
Documentation

The total place-set cardinal s = #S, with all infinite places included.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def totalPlaceCard
    (S : Finset (HeightOneSpectrum (𝓞 K))) : ℕ
theorem

totalPlaceCard_eq_sUnitLogRank_add_one

L40 ↗
KummerTheory.totalPlaceCard_eq_sUnitLogRank_add_one
Documentation

The number of places in the S-unit theorem is one more than the free rank of the S-unit group. The extra coordinate is the roots-of-unity coordinate.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem totalPlaceCard_eq_sUnitLogRank_add_one
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    totalPlaceCard (K := K) S =
      SUnitGroup.logRank (K := K) S + 1
def

multiplicativeZModProductEquivPiSucc

L53 ↗
KummerTheory.multiplicativeZModProductEquivPiSucc
Documentation

One roots-of-unity coordinate together with r free coordinates is the product of r + 1 copies of ZMod n, in multiplicative notation.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · full declaration
def multiplicativeZModProductEquivPiSucc
    (n r : ℕ) :
    Multiplicative (ZMod n) ×
        Multiplicative (Fin r → ZMod n) ≃*
      (Fin (r + 1) → Multiplicative (ZMod n)) where
  toFun x i :=
    Fin.cases x.1
      (fun j => Multiplicative.ofAdd (x.2.toAdd j)) i
  invFun f :=
    (f 0,
      Multiplicative.ofAdd
        (fun j => (f j.succ).toAdd))
  left_inv := by
    rintro ⟨a, b⟩
    apply Prod.ext
    · rfl
    · apply Multiplicative.toAdd.injective
      funext j
      rfl
  right_inv := by
    intro f
    funext i
    refine Fin.cases ?_ (fun j => ?_) i
    · rfl
    · rfl
  map_mul' := by
    intro x y
    funext i
    refine Fin.cases ?_ (fun j => ?_) i
    · rfl
    · rfl
def

finsuppModHom

L86 ↗
KummerTheory.finsuppModHom
Documentation

Coordinatewise reduction of a finite free ℤ-module modulo n.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · full declaration
def finsuppModHom (d n : ℕ) :
    (Fin d →₀ ℤ) →+ (Fin d → ZMod n) where
  toFun x i := x i
  map_zero' := by
    ext i
    simp
  map_add' x y := by
    ext i
    simp
theorem

finsuppModHom_surjective

L97 ↗
KummerTheory.finsuppModHom_surjective
Documentation

Every vector over ZMod n has an integral lift.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem finsuppModHom_surjective (d n : ℕ) :
    Function.Surjective (finsuppModHom d n)
theorem

finsuppModHom_ker

L109 ↗
KummerTheory.finsuppModHom_ker
Documentation

The kernel of coordinatewise reduction is exactly the subgroup of n-fold multiples.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem finsuppModHom_ker (d n : ℕ) :
    (finsuppModHom d n).ker =
      LocalFieldTheory.nsmulAddSubgroup (Fin d →₀ ℤ) n
def

finsuppNsmulQuotientEquivPiZMod

L136 ↗
KummerTheory.finsuppNsmulQuotientEquivPiZMod
Documentation

The finite-free quotient (ℤ^d) / n(ℤ^d) is (ZMod n)^d.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def finsuppNsmulQuotientEquivPiZMod
    (d n : ℕ) :
    (Fin d →₀ ℤ) ⧸
        LocalFieldTheory.nsmulAddSubgroup (Fin d →₀ ℤ) n ≃+
      (Fin d → ZMod n)
def

multiplicativeFinsuppNthPowerQuotientEquivPiZMod

L148 ↗
KummerTheory.multiplicativeFinsuppNthPowerQuotientEquivPiZMod
Documentation

In multiplicative notation, the free integral quotient by n-th powers is a product of copies of ZMod n.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def multiplicativeFinsuppNthPowerQuotientEquivPiZMod
    (d n : ℕ) :
    Multiplicative (Fin d →₀ ℤ) ⧸
        (powMonoidHom n :
          Multiplicative (Fin d →₀ ℤ) →*
            Multiplicative (Fin d →₀ ℤ)).range ≃*
      Multiplicative (Fin d → ZMod n)
instance

finite_finsupp_nsmulQuotient

L161 ↗
KummerTheory.finite_finsupp_nsmulQuotient
Documentation

The quotient of a finite free integral module by a positive multiple is finite.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
instance finite_finsupp_nsmulQuotient
    (d : ℕ) (n : ℕ+) :
    Finite
      ((Fin d →₀ ℤ) ⧸
        LocalFieldTheory.nsmulAddSubgroup
          (Fin d →₀ ℤ) (n : ℕ))
theorem

card_finsupp_nsmulQuotient

L173 ↗
KummerTheory.card_finsupp_nsmulQuotient
Documentation

The cardinality of (ℤ^d) / n(ℤ^d) is n ^ d.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem card_finsupp_nsmulQuotient
    (d : ℕ) (n : ℕ+) :
    Nat.card
        ((Fin d →₀ ℤ) ⧸
          LocalFieldTheory.nsmulAddSubgroup
            (Fin d →₀ ℤ) (n : ℕ)) =
      (n : ℕ) ^ d
theorem

n_dvd_numberField_torsionOrder

L189 ↗
KummerTheory.n_dvd_numberField_torsionOrder
Documentation

A primitive n-th root in K embeds a cyclic subgroup of order n into the roots of unity of the integer ring.

Source context 7 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
omit [NumberField K] in
Lean source · statement
theorem n_dvd_numberField_torsionOrder
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (n : ℕ) ∣ NumberField.Units.torsionOrder K
theorem

card_numberField_torsion_nthPowerQuotient

L224 ↗
KummerTheory.card_numberField_torsion_nthPowerQuotient
Documentation

If K contains a primitive n-th root, the quotient of its roots of unity by n-th powers has cardinality n.

Source context 7 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
include numberFieldK in
Lean source · statement
theorem card_numberField_torsion_nthPowerQuotient
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Nat.card
        (NumberField.Units.torsion K ⧸
          (powMonoidHom (n : ℕ) :
            NumberField.Units.torsion K →*
              NumberField.Units.torsion K).range) =
      (n : ℕ)
def

numberFieldTorsionNthPowerQuotientEquivZMod

L271 ↗
KummerTheory.numberFieldTorsionNthPowerQuotientEquivZMod
Documentation

The roots-of-unity contribution to the S-unit quotient is one copy of ZMod n.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def numberFieldTorsionNthPowerQuotientEquivZMod
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    NumberField.Units.torsion K ⧸
        (powMonoidHom (n : ℕ) :
          NumberField.Units.torsion K →*
            NumberField.Units.torsion K).range ≃*
      Multiplicative (ZMod (n : ℕ))
instance

finite_sUnit_nthPowerQuotient

L296 ↗
KummerTheory.finite_sUnit_nthPowerQuotient
Documentation

The n-th-power quotient of an S-unit group is finite.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
instance finite_sUnit_nthPowerQuotient
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+) :
    Finite
      (SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range)
theorem

card_sUnit_nthPowerQuotient

L315 ↗
KummerTheory.card_sUnit_nthPowerQuotient
Documentation

The S-unit theorem in the form used in the finite S-unit preparation argument:

#(Kˢ / Kˢⁿ) = n ^ (#InfinitePlace K + #S).

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem card_sUnit_nthPowerQuotient
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Nat.card
        (SUnitGroup (K := K) S ⧸
          (powMonoidHom (n : ℕ) :
            SUnitGroup (K := K) S →*
              SUnitGroup (K := K) S).range) =
      (n : ℕ) ^ totalPlaceCard (K := K) S
def

sUnitNthPowerQuotientCoordinates

L390 ↗
KummerTheory.sUnitNthPowerQuotientCoordinates
Documentation

The full S-unit quotient has one torsion coordinate and one coordinate for every logarithmic free generator.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitNthPowerQuotientCoordinates
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range ≃*
      Multiplicative (ZMod (n : ℕ)) ×
        Multiplicative
          (Fin (SUnitGroup.logRank (K := K) S) →
            ZMod (n : ℕ))
theorem

mem_sUnitGroup_of_pow_mem

L423 ↗
KummerTheory.mem_sUnitGroup_of_pow_mem
Documentation

If a positive power of a global unit is an S-unit, then the unit itself is an S-unit. This is the valuation-theoretic saturation needed to compare the abstract Kummer quotient with Kˢ / Kˢⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem mem_sUnitGroup_of_pow_mem
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (n : ℕ+) (x : Kˣ)
    (hx : x ^ (n : ℕ) ∈ SUnitGroup (K := K) S) :
    x ∈ SUnitGroup (K := K) S
def

fullSUnitKummerSubgroup

L444 ↗
KummerTheory.fullSUnitKummerSubgroup
Documentation

The admissible subgroup

Kˢ · Kˣⁿ ≤ Kˣ

whose radical extension is the field N = K(√[n]{Kˢ}) in the finite S-unit preparation argument.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def fullSUnitKummerSubgroup
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    KummerTheory.KummerSubgroup K n
def

sUnitToFullSUnitKummerSubgroup

L453 ↗
KummerTheory.sUnitToFullSUnitKummerSubgroup
Documentation

Include an S-unit in the full S-unit Kummer subgroup.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitToFullSUnitKummerSubgroup
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) S →*
      (fullSUnitKummerSubgroup (K := K) n S).1
def

sUnitToFullSUnitRadicalQuotient

L462 ↗
KummerTheory.sUnitToFullSUnitRadicalQuotient
Documentation

Map an S-unit to its class in (Kˢ · Kˣⁿ) / Kˣⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitToFullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) S →*
      KummerTheory.RestrictedRadicalQuotient
        n (fullSUnitKummerSubgroup (K := K) n S)
theorem

nthPowerSubgroup_le_ker_sUnitToFullSUnitRadicalQuotient

L473 ↗
KummerTheory.nthPowerSubgroup_le_ker_sUnitToFullSUnitRadicalQuotient
Documentation

S-unit n-th powers vanish in the full radical quotient.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem nthPowerSubgroup_le_ker_sUnitToFullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (powMonoidHom (n : ℕ) :
        SUnitGroup (K := K) S →*
          SUnitGroup (K := K) S).range ≤
      MonoidHom.ker
        (sUnitToFullSUnitRadicalQuotient (K := K) n S)
def

sUnitNthPowerQuotientToFullSUnitRadicalQuotient

L499 ↗
KummerTheory.sUnitNthPowerQuotientToFullSUnitRadicalQuotient
Documentation

The canonical comparison

Kˢ / Kˢⁿ → (Kˢ · Kˣⁿ) / Kˣⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitNthPowerQuotientToFullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range →*
      KummerTheory.RestrictedRadicalQuotient
        n (fullSUnitKummerSubgroup (K := K) n S)
theorem

sUnitNthPowerQuotientToFullSUnitRadicalQuotient_surjective

L517 ↗
KummerTheory.sUnitNthPowerQuotientToFullSUnitRadicalQuotient_surjective
Documentation

Every class in (Kˢ · Kˣⁿ) / Kˣⁿ has an S-unit representative.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem sUnitNthPowerQuotientToFullSUnitRadicalQuotient_surjective
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (sUnitNthPowerQuotientToFullSUnitRadicalQuotient
        (K := K) n S)
theorem

sUnitNthPowerQuotientToFullSUnitRadicalQuotient_injective

L552 ↗
KummerTheory.sUnitNthPowerQuotientToFullSUnitRadicalQuotient_injective
Documentation

The canonical comparison from Kˢ / Kˢⁿ is injective. The only arithmetic point is saturation of the S-unit group under positive powers, proved above from valuations.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem sUnitNthPowerQuotientToFullSUnitRadicalQuotient_injective
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Injective
      (sUnitNthPowerQuotientToFullSUnitRadicalQuotient
        (K := K) n S)
def

sUnitNthPowerQuotientEquivFullSUnitRadicalQuotient

L591 ↗
KummerTheory.sUnitNthPowerQuotientEquivFullSUnitRadicalQuotient
Documentation

The exact quotient identification used to define N = K(√[n]{Kˢ}).

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitNthPowerQuotientEquivFullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range ≃*
      KummerTheory.RestrictedRadicalQuotient
        n (fullSUnitKummerSubgroup (K := K) n S)
instance

finite_fullSUnitRadicalQuotient

L609 ↗
KummerTheory.finite_fullSUnitRadicalQuotient
Documentation

The full S-unit radical quotient is finite.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
instance finite_fullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Finite
      (KummerTheory.RestrictedRadicalQuotient
        n (fullSUnitKummerSubgroup (K := K) n S))
theorem

card_fullSUnitRadicalQuotient

L624 ↗
KummerTheory.card_fullSUnitRadicalQuotient
Documentation

The radical quotient defining N has cardinality n ^ s.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem card_fullSUnitRadicalQuotient
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Nat.card
        (KummerTheory.RestrictedRadicalQuotient
          n (fullSUnitKummerSubgroup (K := K) n S)) =
      (n : ℕ) ^ totalPlaceCard (K := K) S

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