Module

Basic.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.Norm.Basic

119 declarations indexed from sourceView source ↗

Module documentation

Integer-valued norm data

This file contains the norm-subgroup lemmas used in local CFT from an abstract integer-valued multiplicative valuation and a norm homomorphism satisfying the standard valuation formula.

Imports2

Imported by4

structure

MultiplicativeIntegerValuation

L27 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation

Documentation

A multiplicative group valuation with values in additive integers.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · full declaration

structure MultiplicativeIntegerValuation (G : Type u) [Group G] where
  /-- The integer valuation of a group element. -/
  val : G → ℤ
  /-- The identity has valuation zero. -/
  map_one : val 1 = 0
  /-- Valuation turns multiplication into integer addition. -/
  map_mul : ∀ x y : G, val (x * y) = val x + val y

theorem

val_inv_eq_zero_of_val_eq_zero

L122 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_inv_eq_zero_of_val_eq_zero

Documentation

Establishes the identity V.val x⁻¹ = 0.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_inv_eq_zero_of_val_eq_zero {x : G} (hx : V.val x = 0) :
    V.val x⁻¹ = 0

theorem

val_pow_eq_zero_iff_of_ne_zero

L135 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_pow_eq_zero_iff_of_ne_zero

Documentation

Characterizes V.val (x ^ n) = 0 by the equivalent condition V.val x = 0.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_pow_eq_zero_iff_of_ne_zero (x : G) {n : ℕ} (hn : n ≠ 0) :
    V.val (x ^ n) = 0 ↔ V.val x = 0

theorem

val_zpow_eq_zero_iff_of_ne_zero

L153 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_zpow_eq_zero_iff_of_ne_zero

Documentation

Characterizes V.val (x ^ n) = 0 by the equivalent condition V.val x = 0.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_zpow_eq_zero_iff_of_ne_zero (x : G) {n : ℤ} (hn : n ≠ 0) :
    V.val (x ^ n) = 0 ↔ V.val x = 0

theorem

valuationHom_ker_eq_zeroSubgroup

L187 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuationHom_ker_eq_zeroSubgroup

Documentation

Establishes the identity V.valuationHom.ker = V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem valuationHom_ker_eq_zeroSubgroup :
    V.valuationHom.ker = V.zeroSubgroup

instance

ofAdd_mem_valueSubgroup_of_exists_val

L224 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofAdd_mem_valueSubgroup_of_exists_val

Documentation

Establishes the membership statement Multiplicative.ofAdd n ∈ V.valueSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem ofAdd_mem_valueSubgroup_of_exists_val {n : ℤ}
    (hn : ∃ x : G, V.val x = n) :
    Multiplicative.ofAdd n ∈ V.valueSubgroup

theorem

exists_val_of_ofAdd_mem_valueSubgroup

L230 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_val_of_ofAdd_mem_valueSubgroup

Documentation

Establishes the identity ∃ x : G, V.val x = n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_val_of_ofAdd_mem_valueSubgroup {n : ℤ}
    (hn : Multiplicative.ofAdd n ∈ V.valueSubgroup) :
    ∃ x : G, V.val x = n

theorem

valueSubgroup_eq_top_of_surjective

L251 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valueSubgroup_eq_top_of_surjective

Documentation

Establishes the identity V.valueSubgroup = ⊤.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem valueSubgroup_eq_top_of_surjective (hV : Function.Surjective V.val) :
    V.valueSubgroup = ⊤

def

quotientZeroSubgroupEquivValueSubgroup

L264 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroupEquivValueSubgroup

Documentation

First-isomorphism-theorem form for an integer-valued valuation: the quotient by valuation-zero elements is the value subgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def quotientZeroSubgroupEquivValueSubgroup :
    G ⧸ V.zeroSubgroup ≃* V.valueSubgroup

theorem

quotientZeroSubgroupEquivValueSubgroup_mk

L274 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroupEquivValueSubgroup_mk

Documentation

Establishes the identity V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup x) = V.valuationHom.rangeRestrict x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroupEquivValueSubgroup_mk (x : G) :
    V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup x) =
      V.valuationHom.rangeRestrict x

theorem

coe_quotientZeroSubgroupEquivValueSubgroup_mk

L284 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.coe_quotientZeroSubgroupEquivValueSubgroup_mk

Documentation

Establishes the identity ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) : Multiplicative ℤ) = Multiplicative.ofAdd (V.val x).

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem coe_quotientZeroSubgroupEquivValueSubgroup_mk (x : G) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) :
      Multiplicative ℤ) =
      Multiplicative.ofAdd (V.val x)

theorem

toAdd_quotientZeroSubgroupEquivValueSubgroup_mk

L296 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.toAdd_quotientZeroSubgroupEquivValueSubgroup_mk

Documentation

Establishes the identity Multiplicative.toAdd (((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) : Multiplicative ℤ)) = V.val x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem toAdd_quotientZeroSubgroupEquivValueSubgroup_mk (x : G) :
    Multiplicative.toAdd
      (((V.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) :
        Multiplicative ℤ)) = V.val x

theorem

toAdd_quotientZeroSubgroupEquivValueSubgroup_div_mk

L308 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.toAdd_quotientZeroSubgroupEquivValueSubgroup_div_mk

Documentation

Establishes the identity Multiplicative.toAdd (((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) : Multiplicative ℤ)) = V.val x - V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem toAdd_quotientZeroSubgroupEquivValueSubgroup_div_mk
    (x y : G) :
    Multiplicative.toAdd
      (((V.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) :
        Multiplicative ℤ)) = V.val x - V.val y

theorem

quotientZeroSubgroup_value_mem_integerMultipleSubgroup_iff

L321 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_value_mem_integerMultipleSubgroup_iff

Documentation

Characterizes ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup d by the equivalent condition d ∣ V.val x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_value_mem_integerMultipleSubgroup_iff
    (d : ℤ) (x : G) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) :
      Multiplicative ℤ) ∈ integerMultipleSubgroup d ↔ d ∣ V.val x

theorem

quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_iff

L334 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_iff

Documentation

Characterizes ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup d by the equivalent condition d ∣ V.val x - V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_iff
    (d : ℤ) (x y : G) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) :
      Multiplicative ℤ) ∈ integerMultipleSubgroup d ↔
      d ∣ V.val x - V.val y

theorem

quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_dvd_val

L348 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_dvd_val

Documentation

Establishes the membership statement ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup d.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_value_mem_integerMultipleSubgroup_of_dvd_val
    {d : ℤ} {x : G} (hx : d ∣ V.val x) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) :
      Multiplicative ℤ) ∈ integerMultipleSubgroup d

theorem

dvd_val_of_quotientZeroSubgroup_value_mem_integerMultipleSubgroup

L356 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.dvd_val_of_quotientZeroSubgroup_value_mem_integerMultipleSubgroup

Documentation

Establishes the divisibility statement d ∣ V.val x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem dvd_val_of_quotientZeroSubgroup_value_mem_integerMultipleSubgroup
    {d : ℤ} {x : G}
    (hx :
      ((V.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' V.zeroSubgroup x) : V.valueSubgroup) :
        Multiplicative ℤ) ∈ integerMultipleSubgroup d) :
    d ∣ V.val x

theorem

quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_dvd

L370 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_dvd

Documentation

Establishes the membership statement ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) : Multiplicative ℤ) ∈ integerMultipleSubgroup d.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup_of_dvd
    {d : ℤ} {x y : G} (hxy : d ∣ V.val x - V.val y) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) :
      Multiplicative ℤ) ∈ integerMultipleSubgroup d

theorem

dvd_of_quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup

L378 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.dvd_of_quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup

Documentation

Establishes the divisibility statement d ∣ V.val x - V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem dvd_of_quotientZeroSubgroup_value_div_mem_integerMultipleSubgroup
    {d : ℤ} {x y : G}
    (hxy :
      ((V.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' V.zeroSubgroup (x / y)) : V.valueSubgroup) :
        Multiplicative ℤ) ∈ integerMultipleSubgroup d) :
    d ∣ V.val x - V.val y

def

quotientZeroSubgroupEquivMultiplicativeInt

L389 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroupEquivMultiplicativeInt

Documentation

If the valuation is surjective, the quotient by valuation-zero elements is the full multiplicative copy of ℤ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def quotientZeroSubgroupEquivMultiplicativeInt
    (hV : Function.Surjective V.val) :
    G ⧸ V.zeroSubgroup ≃* Multiplicative ℤ

def

IsUniformizer

L397 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.IsUniformizer

Documentation

A multiplicative element of valuation one.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def IsUniformizer (ϖ : G) : Prop

def

HasUniformizer

L401 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.HasUniformizer

Documentation

Existence of a multiplicative element of valuation one.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def HasUniformizer : Prop

theorem

hasUniformizer_of_surjective

L405 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasUniformizer_of_surjective

Documentation

A surjective integer valuation has an element of valuation one.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem hasUniformizer_of_surjective (hV : Function.Surjective V.val) :
    V.HasUniformizer

theorem

exists_uniformizer_of_surjective

L411 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_uniformizer_of_surjective

Documentation

Surjectivity of the integer valuation yields a uniformizer.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_uniformizer_of_surjective (hV : Function.Surjective V.val) :
    ∃ ϖ : G, V.IsUniformizer ϖ

theorem

val_uniformizer_zpow

L416 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_uniformizer_zpow

Documentation

val_uniformizer satisfies the integer-power formula V.val (ϖ ^ n) = n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_uniformizer_zpow {ϖ : G} (hϖ : V.IsUniformizer ϖ)
    (n : ℤ) :
    V.val (ϖ ^ n) = n

theorem

val_uniformizer_pow

L422 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_uniformizer_pow

Documentation

val_uniformizer satisfies the natural-power formula V.val (ϖ ^ n) = (n : ℤ).

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_uniformizer_pow {ϖ : G} (hϖ : V.IsUniformizer ϖ)
    (n : ℕ) :
    V.val (ϖ ^ n) = (n : ℤ)

theorem

uniformizer_zpow_mem_zeroSubgroup_iff

L428 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.uniformizer_zpow_mem_zeroSubgroup_iff

Documentation

Characterizes ϖ ^ n ∈ V.zeroSubgroup by the equivalent condition n = 0.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem uniformizer_zpow_mem_zeroSubgroup_iff {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (n : ℤ) :
    ϖ ^ n ∈ V.zeroSubgroup ↔ n = 0

theorem

uniformizer_pow_mem_zeroSubgroup_iff

L434 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.uniformizer_pow_mem_zeroSubgroup_iff

Documentation

Characterizes ϖ ^ n ∈ V.zeroSubgroup by the equivalent condition n = 0.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem uniformizer_pow_mem_zeroSubgroup_iff {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (n : ℕ) :
    ϖ ^ n ∈ V.zeroSubgroup ↔ n = 0

theorem

val_surjective_of_uniformizer

L441 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_surjective_of_uniformizer

Documentation

The specified map is surjective: Function.Surjective V.val.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_surjective_of_uniformizer {ϖ : G} (hϖ : V.IsUniformizer ϖ) :
    Function.Surjective V.val

theorem

hasUniformizer_iff_val_surjective

L447 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasUniformizer_iff_val_surjective

Documentation

Characterizes V.HasUniformizer by the equivalent condition Function.Surjective V.val.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem hasUniformizer_iff_val_surjective :
    V.HasUniformizer ↔ Function.Surjective V.val

theorem

valueSubgroup_eq_top_of_uniformizer

L455 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valueSubgroup_eq_top_of_uniformizer

Documentation

Establishes the identity V.valueSubgroup = ⊤.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem valueSubgroup_eq_top_of_uniformizer {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) :
    V.valueSubgroup = ⊤

def

quotientZeroSubgroupEquivMultiplicativeIntOfUniformizer

L463 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroupEquivMultiplicativeIntOfUniformizer

Documentation

Uniformizer form of the quotient equivalence G / G⁰ ≃ Multiplicative ℤ. The uniformizer proves that the value group is all of ℤ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def quotientZeroSubgroupEquivMultiplicativeIntOfUniformizer
    {ϖ : G} (hϖ : V.IsUniformizer ϖ) :
    G ⧸ V.zeroSubgroup ≃* Multiplicative ℤ

theorem

coe_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow

L474 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.coe_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow

Documentation

coe_quotientZeroSubgroupEquivValueSubgroup_uniformizer satisfies the integer-power formula ((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup (ϖ ^ n)) : V.valueSubgroup) : Multiplicative ℤ) = Multiplicative.ofAdd n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem coe_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow
    {ϖ : G} (hϖ : V.IsUniformizer ϖ) (n : ℤ) :
    ((V.quotientZeroSubgroupEquivValueSubgroup
        (QuotientGroup.mk' V.zeroSubgroup (ϖ ^ n)) : V.valueSubgroup) :
      Multiplicative ℤ) = Multiplicative.ofAdd n

theorem

toAdd_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow

L487 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.toAdd_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow

Documentation

toAdd_quotientZeroSubgroupEquivValueSubgroup_uniformizer satisfies the integer-power formula Multiplicative.toAdd (((V.quotientZeroSubgroupEquivValueSubgroup (QuotientGroup.mk' V.zeroSubgroup (ϖ ^ n)) : V.valueSubgroup) : Multiplicative ℤ)) = n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem toAdd_quotientZeroSubgroupEquivValueSubgroup_uniformizer_zpow
    {ϖ : G} (hϖ : V.IsUniformizer ϖ) (n : ℤ) :
    Multiplicative.toAdd
      (((V.quotientZeroSubgroupEquivValueSubgroup
          (QuotientGroup.mk' V.zeroSubgroup (ϖ ^ n)) : V.valueSubgroup) :
        Multiplicative ℤ)) = n

structure

UnitUniformizerDecomposition

L498 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition

Documentation

A representative-level decomposition x = u * ϖ^n, with u of valuation zero. This is the abstract multiplicative form of Kˣ = O_Kˣ · ϖ^ℤ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · full declaration

structure UnitUniformizerDecomposition (ϖ x : G) where
  /-- The valuation-zero factor. -/
  unitPart : G
  /-- The unit factor has valuation zero. -/
  unit_mem : unitPart ∈ V.zeroSubgroup
  /-- The exponent of the chosen uniformizer. -/
  exponent : ℤ
  /-- Reconstruction from the unit factor and uniformizer power. -/
  eq_unit_mul_zpow : x = unitPart * ϖ ^ exponent

def

HasUnitUniformizerDecomposition

L509 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.HasUnitUniformizerDecomposition

Documentation

Every element admits a unit-uniformizer decomposition with respect to ϖ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

def HasUnitUniformizerDecomposition (ϖ : G) : Prop

def

canonicalUnitUniformizerDecomposition

L513 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.canonicalUnitUniformizerDecomposition

Documentation

The canonical unit-uniformizer decomposition attached to a uniformizer.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · full declaration

def canonicalUnitUniformizerDecomposition {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) :
    V.UnitUniformizerDecomposition ϖ x where
  unitPart := x * ϖ ^ (-(V.val x))
  unit_mem := by
    rw [V.mem_zeroSubgroup_iff, V.val_mul, V.val_zpow, hϖ]
    ring
  exponent := V.val x
  eq_unit_mul_zpow := by
    calc
      x = x * 1 := by rw [mul_one]
      _ = x * (ϖ ^ (-(V.val x)) * ϖ ^ V.val x) := by
        rw [← zpow_add, neg_add_cancel, zpow_zero]
      _ = (x * ϖ ^ (-(V.val x))) * ϖ ^ V.val x := by
        rw [mul_assoc]

theorem

hasUnitUniformizerDecomposition_of_uniformizer

L532 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasUnitUniformizerDecomposition_of_uniformizer

Documentation

A chosen uniformizer gives a unit-times-uniformizer-power decomposition of every group element.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem hasUnitUniformizerDecomposition_of_uniformizer {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) :
    V.HasUnitUniformizerDecomposition ϖ

theorem

unitUniformizerDecomposition

L542 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.unitUniformizerDecomposition

Documentation

Every group element has a unit-times-uniformizer-power decomposition relative to a chosen uniformizer.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem unitUniformizerDecomposition {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) :
    Nonempty (V.UnitUniformizerDecomposition ϖ x)

theorem

exists_zeroSubgroup_mul_uniformizer_zpow

L551 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_zeroSubgroup_mul_uniformizer_zpow

Documentation

exists_zeroSubgroup_mul_uniformizer satisfies the integer-power formula ∃ u : G, u ∈ V.zeroSubgroup ∧ ∃ n : ℤ, x = u * ϖ ^ n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_zeroSubgroup_mul_uniformizer_zpow {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ ∃ n : ℤ, x = u * ϖ ^ n

theorem

exists_zeroSubgroup_mul_uniformizer_zpow_eq

L558 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_zeroSubgroup_mul_uniformizer_zpow_eq

Documentation

Establishes the identity ∃ u : G, u ∈ V.zeroSubgroup ∧ u * ϖ ^ V.val x = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_zeroSubgroup_mul_uniformizer_zpow_eq {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ u * ϖ ^ V.val x = x

theorem

val_eq_iff_exists_zeroSubgroup_mul_uniformizer_zpow

L568 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_iff_exists_zeroSubgroup_mul_uniformizer_zpow

Documentation

Characterizes V.val x = n by the equivalent condition ∃ u : G, u ∈ V.zeroSubgroup ∧ u * ϖ ^ n = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_iff_exists_zeroSubgroup_mul_uniformizer_zpow {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) (n : ℤ) :
    V.val x = n ↔ ∃ u : G, u ∈ V.zeroSubgroup ∧ u * ϖ ^ n = x

theorem

val_eq_iff_exists_eq_zeroSubgroup_mul_uniformizer_zpow

L586 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_iff_exists_eq_zeroSubgroup_mul_uniformizer_zpow

Documentation

Characterizes V.val x = n by the equivalent condition ∃ u : G, u ∈ V.zeroSubgroup ∧ x = u * ϖ ^ n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_iff_exists_eq_zeroSubgroup_mul_uniformizer_zpow {ϖ : G}
    (hϖ : V.IsUniformizer ϖ) (x : G) (n : ℤ) :
    V.val x = n ↔ ∃ u : G, u ∈ V.zeroSubgroup ∧ x = u * ϖ ^ n

theorem

unitPart_val_zero

L604 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unitPart_val_zero

Documentation

Establishes the identity V.val d.unitPart = 0.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unitPart_val_zero
    (d : V.UnitUniformizerDecomposition ϖ x) :
    V.val d.unitPart = 0

theorem

val_eq_exponent

L611 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.val_eq_exponent

Documentation

The valuation of the represented element is the exponent when ϖ is a uniformizer.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem val_eq_exponent (hϖ : V.IsUniformizer ϖ)
    (d : V.UnitUniformizerDecomposition ϖ x) :
    V.val x = d.exponent

theorem

unitPart_eq_mul_inv_zpow

L628 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unitPart_eq_mul_inv_zpow

Documentation

The unit part is recovered from the represented element and the recorded exponent.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unitPart_eq_mul_inv_zpow
    (d : V.UnitUniformizerDecomposition ϖ x) :
    d.unitPart = x * (ϖ ^ d.exponent)⁻¹

theorem

unitPart_unique_of_exponent_eq

L639 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unitPart_unique_of_exponent_eq

Documentation

If two decompositions use the same exponent, then their unit parts agree.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unitPart_unique_of_exponent_eq
    (d₁ d₂ : V.UnitUniformizerDecomposition ϖ x)
    (h : d₁.exponent = d₂.exponent) :
    d₁.unitPart = d₂.unitPart

theorem

exponent_unique

L646 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.exponent_unique

Documentation

The exponent in a unit-uniformizer decomposition is unique.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem exponent_unique (hϖ : V.IsUniformizer ϖ)
    (d₁ d₂ : V.UnitUniformizerDecomposition ϖ x) :
    d₁.exponent = d₂.exponent

theorem

unitPart_unique

L655 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unitPart_unique

Documentation

The unit part in a unit-uniformizer decomposition is unique once the uniformizer is fixed.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unitPart_unique (hϖ : V.IsUniformizer ϖ)
    (d₁ d₂ : V.UnitUniformizerDecomposition ϖ x) :
    d₁.unitPart = d₂.unitPart

theorem

val_unit_mul_zpow

L662 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.val_unit_mul_zpow

Documentation

A valuation-zero multiple of a uniformizer power has valuation equal to the exponent.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem val_unit_mul_zpow (hϖ : V.IsUniformizer ϖ)
    {u : G} (hu : u ∈ V.zeroSubgroup) (n : ℤ) :
    V.val (u * ϖ ^ n) = n

theorem

val_uniformizer_zpow

L669 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.val_uniformizer_zpow

Documentation

A uniformizer power has valuation equal to its exponent.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem val_uniformizer_zpow (hϖ : V.IsUniformizer ϖ) (n : ℤ) :
    V.val (ϖ ^ n) = n

theorem

val_uniformizer_pow

L675 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.val_uniformizer_pow

Documentation

A natural power of a uniformizer has valuation equal to the natural exponent.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem val_uniformizer_pow (hϖ : V.IsUniformizer ϖ) (n : ℕ) :
    V.val (ϖ ^ n) = (n : ℤ)

theorem

exponent_unique_of_unit_mul_eq

L681 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.exponent_unique_of_unit_mul_eq

Documentation

Equality of two unit-uniformizer normal forms forces equality of exponents.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem exponent_unique_of_unit_mul_eq (hϖ : V.IsUniformizer ϖ)
    {u w : G} (hu : u ∈ V.zeroSubgroup) (hw : w ∈ V.zeroSubgroup)
    {m n : ℤ} (h : u * ϖ ^ m = w * ϖ ^ n) :
    m = n

theorem

unit_mul_zpow_eq_iff

L691 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unit_mul_zpow_eq_iff

Documentation

Equality of two unit-uniformizer normal forms is equivalent to equality of both the unit part and exponent.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unit_mul_zpow_eq_iff (hϖ : V.IsUniformizer ϖ)
    {u w : G} (hu : u ∈ V.zeroSubgroup) (hw : w ∈ V.zeroSubgroup)
    {m n : ℤ} :
    u * ϖ ^ m = w * ϖ ^ n ↔ u = w ∧ m = n

theorem

unit_mul_zpow_eq_iff_exponent_eq_and_unit_eq

L715 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.UnitUniformizerDecomposition.unit_mul_zpow_eq_iff_exponent_eq_and_unit_eq

Documentation

Equality of two unit-uniformizer normal forms is equivalent to equality of exponents together with equality of unit parts.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)
namespace UnitUniformizerDecomposition
variable {V : MultiplicativeIntegerValuation G} {ϖ x : G}

Lean source · statement

theorem unit_mul_zpow_eq_iff_exponent_eq_and_unit_eq
    (hϖ : V.IsUniformizer ϖ)
    {u w : G} (hu : u ∈ V.zeroSubgroup) (hw : w ∈ V.zeroSubgroup)
    {m n : ℤ} :
    u * ϖ ^ m = w * ϖ ^ n ↔ m = n ∧ u = w

theorem

uniformizer_exponent_unique

L730 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.uniformizer_exponent_unique

Documentation

Establishes the identity d₁.exponent = d₂.exponent.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem uniformizer_exponent_unique {ϖ x : G}
    (hϖ : V.IsUniformizer ϖ)
    (d₁ d₂ : V.UnitUniformizerDecomposition ϖ x) :
    d₁.exponent = d₂.exponent

theorem

uniformizer_unitPart_unique

L737 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.uniformizer_unitPart_unique

Documentation

Establishes the identity d₁.unitPart = d₂.unitPart.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem uniformizer_unitPart_unique {ϖ x : G}
    (hϖ : V.IsUniformizer ϖ)
    (d₁ d₂ : V.UnitUniformizerDecomposition ϖ x) :
    d₁.unitPart = d₂.unitPart

theorem

valuation_uniformizer_normal_form

L744 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_uniformizer_normal_form

Documentation

Establishes the identity V.val (u * ϖ ^ n) = n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem valuation_uniformizer_normal_form {ϖ u : G}
    (hϖ : V.IsUniformizer ϖ) (hu : u ∈ V.zeroSubgroup) (n : ℤ) :
    V.val (u * ϖ ^ n) = n

theorem

unit_uniformizer_normal_form_eq_iff

L750 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.unit_uniformizer_normal_form_eq_iff

Documentation

Characterizes u * ϖ ^ m = w * ϖ ^ n by the equivalent condition u = w ∧ m = n.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem unit_uniformizer_normal_form_eq_iff {ϖ u w : G}
    (hϖ : V.IsUniformizer ϖ) (hu : u ∈ V.zeroSubgroup)
    (hw : w ∈ V.zeroSubgroup) {m n : ℤ} :
    u * ϖ ^ m = w * ϖ ^ n ↔ u = w ∧ m = n

theorem

zeroSubgroup_mul_mem

L757 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_mul_mem

Documentation

Establishes the membership statement x * y ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_mul_mem {x y : G}
    (hx : x ∈ V.zeroSubgroup) (hy : y ∈ V.zeroSubgroup) :
    x * y ∈ V.zeroSubgroup

theorem

zeroSubgroup_inv_mem

L763 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_inv_mem

Documentation

Establishes the membership statement x⁻¹ ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_inv_mem {x : G} (hx : x ∈ V.zeroSubgroup) :
    x⁻¹ ∈ V.zeroSubgroup

theorem

zeroSubgroup_div_mem

L768 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_div_mem

Documentation

Establishes the membership statement x / y ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_div_mem {x y : G}
    (hx : x ∈ V.zeroSubgroup) (hy : y ∈ V.zeroSubgroup) :
    x / y ∈ V.zeroSubgroup

theorem

div_mem_zeroSubgroup_iff

L775 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.div_mem_zeroSubgroup_iff

Documentation

Characterizes x / y ∈ V.zeroSubgroup by the equivalent condition V.val x = V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem div_mem_zeroSubgroup_iff (x y : G) :
    x / y ∈ V.zeroSubgroup ↔ V.val x = V.val y

theorem

val_eq_of_div_mem_zeroSubgroup

L781 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_of_div_mem_zeroSubgroup

Documentation

Establishes the identity V.val x = V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_of_div_mem_zeroSubgroup {x y : G}
    (hxy : x / y ∈ V.zeroSubgroup) :
    V.val x = V.val y

theorem

div_mem_zeroSubgroup_of_val_eq

L787 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.div_mem_zeroSubgroup_of_val_eq

Documentation

Establishes the membership statement x / y ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem div_mem_zeroSubgroup_of_val_eq {x y : G} (hxy : V.val x = V.val y) :
    x / y ∈ V.zeroSubgroup

theorem

div_mem_zeroSubgroup_iff_inv_mul_mem_zeroSubgroup

L793 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.div_mem_zeroSubgroup_iff_inv_mul_mem_zeroSubgroup

Documentation

In the valuation-zero subgroup, the right quotient x / y and the left quotient y⁻¹ * x give the same membership test.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem div_mem_zeroSubgroup_iff_inv_mul_mem_zeroSubgroup (x y : G) :
    x / y ∈ V.zeroSubgroup ↔ y⁻¹ * x ∈ V.zeroSubgroup

theorem

inv_mul_mem_zeroSubgroup_iff_div_mem_zeroSubgroup

L801 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.inv_mul_mem_zeroSubgroup_iff_div_mem_zeroSubgroup

Documentation

Left-quotient version of div_mem_zeroSubgroup_iff_inv_mul_mem_zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem inv_mul_mem_zeroSubgroup_iff_div_mem_zeroSubgroup (x y : G) :
    y⁻¹ * x ∈ V.zeroSubgroup ↔ x / y ∈ V.zeroSubgroup

theorem

inv_mul_mem_zeroSubgroup_iff

L806 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.inv_mul_mem_zeroSubgroup_iff

Documentation

Left-quotient version of div_mem_zeroSubgroup_iff.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem inv_mul_mem_zeroSubgroup_iff (x y : G) :
    y⁻¹ * x ∈ V.zeroSubgroup ↔ V.val x = V.val y

theorem

val_eq_of_inv_mul_mem_zeroSubgroup

L812 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_of_inv_mul_mem_zeroSubgroup

Documentation

Establishes the identity V.val x = V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_of_inv_mul_mem_zeroSubgroup {x y : G}
    (hxy : y⁻¹ * x ∈ V.zeroSubgroup) :
    V.val x = V.val y

theorem

inv_mul_mem_zeroSubgroup_of_val_eq

L818 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.inv_mul_mem_zeroSubgroup_of_val_eq

Documentation

Establishes the membership statement y⁻¹ * x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem inv_mul_mem_zeroSubgroup_of_val_eq {x y : G}
    (hxy : V.val x = V.val y) :
    y⁻¹ * x ∈ V.zeroSubgroup

theorem

quotientZeroSubgroup_mk_eq_iff_div_mem

L824 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_mk_eq_iff_div_mem

Documentation

Equality in G ⧸ zeroSubgroup, in right-quotient form.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_mk_eq_iff_div_mem (x y : G) :
    QuotientGroup.mk' V.zeroSubgroup x =
        QuotientGroup.mk' V.zeroSubgroup y ↔
      x / y ∈ V.zeroSubgroup

theorem

quotientZeroSubgroup_mk_eq_iff_inv_mul_mem

L833 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_mk_eq_iff_inv_mul_mem

Documentation

Equality in G ⧸ zeroSubgroup, in left-quotient form.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_mk_eq_iff_inv_mul_mem (x y : G) :
    QuotientGroup.mk' V.zeroSubgroup x =
        QuotientGroup.mk' V.zeroSubgroup y ↔
      y⁻¹ * x ∈ V.zeroSubgroup

theorem

quotientZeroSubgroup_mk_eq_iff_val_eq

L841 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.quotientZeroSubgroup_mk_eq_iff_val_eq

Documentation

Equality in G ⧸ zeroSubgroup is equality of valuations.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem quotientZeroSubgroup_mk_eq_iff_val_eq (x y : G) :
    QuotientGroup.mk' V.zeroSubgroup x =
        QuotientGroup.mk' V.zeroSubgroup y ↔
      V.val x = V.val y

theorem

div_mem_zeroSubgroup_iff_exists_zeroSubgroup_mul_eq

L852 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.div_mem_zeroSubgroup_iff_exists_zeroSubgroup_mul_eq

Documentation

Two elements have quotient in the zero-valuation subgroup exactly when the left element is the right element multiplied on the left by a zero-valuation element. This is the right-coset representative form used in Kˣ / O_Kˣ calculations.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem div_mem_zeroSubgroup_iff_exists_zeroSubgroup_mul_eq (x y : G) :
    x / y ∈ V.zeroSubgroup ↔
      ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x

theorem

exists_zeroSubgroup_mul_eq_of_div_mem_zeroSubgroup

L865 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_zeroSubgroup_mul_eq_of_div_mem_zeroSubgroup

Documentation

Establishes the identity ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_zeroSubgroup_mul_eq_of_div_mem_zeroSubgroup
    {x y : G} (hxy : x / y ∈ V.zeroSubgroup) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x

theorem

div_mem_zeroSubgroup_of_exists_zeroSubgroup_mul_eq

L871 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.div_mem_zeroSubgroup_of_exists_zeroSubgroup_mul_eq

Documentation

Establishes the membership statement x / y ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem div_mem_zeroSubgroup_of_exists_zeroSubgroup_mul_eq
    {x y : G} (hxy : ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x) :
    x / y ∈ V.zeroSubgroup

theorem

inv_mul_mem_zeroSubgroup_iff_exists_mul_zeroSubgroup_eq

L879 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.inv_mul_mem_zeroSubgroup_iff_exists_mul_zeroSubgroup_eq

Documentation

Two elements have left quotient in the zero-valuation subgroup exactly when the left element is the right element multiplied on the right by a zero-valuation element.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem inv_mul_mem_zeroSubgroup_iff_exists_mul_zeroSubgroup_eq (x y : G) :
    y⁻¹ * x ∈ V.zeroSubgroup ↔
      ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x

theorem

exists_mul_zeroSubgroup_eq_of_inv_mul_mem_zeroSubgroup

L892 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_mul_zeroSubgroup_eq_of_inv_mul_mem_zeroSubgroup

Documentation

Establishes the identity ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_mul_zeroSubgroup_eq_of_inv_mul_mem_zeroSubgroup
    {x y : G} (hxy : y⁻¹ * x ∈ V.zeroSubgroup) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x

theorem

inv_mul_mem_zeroSubgroup_of_exists_mul_zeroSubgroup_eq

L898 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.inv_mul_mem_zeroSubgroup_of_exists_mul_zeroSubgroup_eq

Documentation

Establishes the membership statement y⁻¹ * x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem inv_mul_mem_zeroSubgroup_of_exists_mul_zeroSubgroup_eq
    {x y : G} (hxy : ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x) :
    y⁻¹ * x ∈ V.zeroSubgroup

theorem

val_eq_iff_exists_zeroSubgroup_mul_eq

L907 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_iff_exists_zeroSubgroup_mul_eq

Documentation

Characterizes V.val x = V.val y by the equivalent condition ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_iff_exists_zeroSubgroup_mul_eq (x y : G) :
    V.val x = V.val y ↔
      ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x

theorem

val_eq_iff_exists_mul_zeroSubgroup_eq

L917 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_iff_exists_mul_zeroSubgroup_eq

Documentation

Characterizes V.val x = V.val y by the equivalent condition ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_iff_exists_mul_zeroSubgroup_eq (x y : G) :
    V.val x = V.val y ↔
      ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x

theorem

exists_zeroSubgroup_mul_eq_of_val_eq

L924 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_zeroSubgroup_mul_eq_of_val_eq

Documentation

Establishes the identity ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_zeroSubgroup_mul_eq_of_val_eq {x y : G}
    (hxy : V.val x = V.val y) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x

theorem

exists_mul_zeroSubgroup_eq_of_val_eq

L930 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_mul_zeroSubgroup_eq_of_val_eq

Documentation

Establishes the identity ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem exists_mul_zeroSubgroup_eq_of_val_eq {x y : G}
    (hxy : V.val x = V.val y) :
    ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x

theorem

val_eq_of_exists_zeroSubgroup_mul_eq

L936 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_of_exists_zeroSubgroup_mul_eq

Documentation

Establishes the identity V.val x = V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_of_exists_zeroSubgroup_mul_eq {x y : G}
    (hxy : ∃ u : G, u ∈ V.zeroSubgroup ∧ u * y = x) :
    V.val x = V.val y

theorem

val_eq_of_exists_mul_zeroSubgroup_eq

L942 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_of_exists_mul_zeroSubgroup_eq

Documentation

Establishes the identity V.val x = V.val y.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_of_exists_mul_zeroSubgroup_eq {x y : G}
    (hxy : ∃ u : G, u ∈ V.zeroSubgroup ∧ y * u = x) :
    V.val x = V.val y

theorem

val_eq_zero_iff_mem_zeroSubgroup

L948 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_zero_iff_mem_zeroSubgroup

Documentation

Characterizes V.val x = 0 by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_zero_iff_mem_zeroSubgroup (x : G) :
    V.val x = 0 ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_pow_mem

L953 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_pow_mem

Documentation

Establishes the membership statement x ^ n ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_pow_mem {x : G} (hx : x ∈ V.zeroSubgroup) (n : ℕ) :
    x ^ n ∈ V.zeroSubgroup

theorem

zeroSubgroup_zpow_mem

L958 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_zpow_mem

Documentation

Establishes the membership statement x ^ n ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_zpow_mem {x : G} (hx : x ∈ V.zeroSubgroup) (n : ℤ) :
    x ^ n ∈ V.zeroSubgroup

theorem

zeroSubgroup_pow_mem_iff_of_ne_zero

L963 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_pow_mem_iff_of_ne_zero

Documentation

Characterizes x ^ n ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_pow_mem_iff_of_ne_zero (x : G) {n : ℕ} (hn : n ≠ 0) :
    x ^ n ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_zpow_mem_iff_of_ne_zero

L970 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_zpow_mem_iff_of_ne_zero

Documentation

Characterizes x ^ n ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_zpow_mem_iff_of_ne_zero (x : G) {n : ℤ} (hn : n ≠ 0) :
    x ^ n ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_mul_iff_right

L977 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_mul_iff_right

Documentation

Characterizes x * u ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_mul_iff_right {x u : G} (hu : u ∈ V.zeroSubgroup) :
    x * u ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_mul_iff_left

L988 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_mul_iff_left

Documentation

Characterizes u * x ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_mul_iff_left {u x : G} (hu : u ∈ V.zeroSubgroup) :
    u * x ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_div_iff_right

L999 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_div_iff_right

Documentation

Characterizes x / u ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_div_iff_right {x u : G} (hu : u ∈ V.zeroSubgroup) :
    x / u ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

zeroSubgroup_div_iff_left

L1006 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zeroSubgroup_div_iff_left

Documentation

Characterizes u / x ∈ V.zeroSubgroup by the equivalent condition x ∈ V.zeroSubgroup.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem zeroSubgroup_div_iff_left {u x : G} (hu : u ∈ V.zeroSubgroup) :
    u / x ∈ V.zeroSubgroup ↔ x ∈ V.zeroSubgroup

theorem

val_mul_eq_left_of_right_zero

L1017 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_mul_eq_left_of_right_zero

Documentation

Establishes the identity V.val (x * u) = V.val x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_mul_eq_left_of_right_zero {x u : G} (hu : V.val u = 0) :
    V.val (x * u) = V.val x

theorem

val_mul_eq_right_of_left_zero

L1022 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_mul_eq_right_of_left_zero

Documentation

Establishes the identity V.val (u * x) = V.val x.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_mul_eq_right_of_left_zero {u x : G} (hu : V.val u = 0) :
    V.val (u * x) = V.val x

theorem

val_zeroSubgroup_mul_zpow

L1027 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_zeroSubgroup_mul_zpow

Documentation

val_zeroSubgroup_mul satisfies the integer-power formula V.val (u * γ ^ n) = n * V.val γ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_zeroSubgroup_mul_zpow {u γ : G}
    (hu : u ∈ V.zeroSubgroup) (n : ℤ) :
    V.val (u * γ ^ n) = n * V.val γ

theorem

val_subgroup_mul_zpow_of_le_zeroSubgroup

L1033 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_subgroup_mul_zpow_of_le_zeroSubgroup

Documentation

Establishes the identity V.val (u * γ ^ n) = n * V.val γ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_subgroup_mul_zpow_of_le_zeroSubgroup
    (P : Subgroup G) (hP : P ≤ V.zeroSubgroup)
    {u γ : G} (hu : u ∈ P) (n : ℤ) :
    V.val (u * γ ^ n) = n * V.val γ

theorem

val_eq_generator_multiple_of_mem_subgroup_mul_zpow

L1043 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.val_eq_generator_multiple_of_mem_subgroup_mul_zpow

Documentation

val_eq_generator_multiple_of_mem_subgroup_mul satisfies the integer-power formula V.val x = n * V.val γ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {G : Type u} [Group G] (V : MultiplicativeIntegerValuation G)

Lean source · statement

theorem val_eq_generator_multiple_of_mem_subgroup_mul_zpow
    (P : Subgroup G) (hP : P ≤ V.zeroSubgroup)
    {x u γ : G} (hu : u ∈ P) {n : ℤ}
    (hx : x = u * γ ^ n) :
    V.val x = n * V.val γ

structure

ValuedNorm

L1061 ↗

LocalFieldTheory.DiscreteValuationField.ValuedNorm

Documentation

A norm-like homomorphism compatible with integer-valued valuations.

residueDegree is proof-attached data: it is the multiplier in valuation_formula, not an independent field-extension invariant. In the usual discrete-valued application the source has a uniformizer, and evaluating valuation_formula at that uniformizer uniquely determines this coefficient. The generic group-level abstraction does not require a uniformizer, so it keeps the coefficient together with the formula that certifies it.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · full declaration

structure ValuedNorm {G : Type u} {H : Type v} [Group G] [Group H]
    (vG : MultiplicativeIntegerValuation G)
    (vH : MultiplicativeIntegerValuation H) where
  /-- The multiplicative norm homomorphism. -/
  toHom : H →* G
  /-- The nonnegative scaling factor in the valuation formula. -/
  residueDegree : ℕ
  /-- Applying the norm scales valuation by the residue-degree factor. -/
  valuation_formula :
    ∀ x : H, vG.val (toHom x) = (residueDegree : ℤ) * vH.val x

Module documentation

Integer-valued norm data

Declarations