Theorems · Theorem · commutative algebra

Valuation.IsRankOneDiscrete.generator_zpowers_eq_range

∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [inst_1 : Field K] (w : Valuation K Γ)
  [inst_2 : w.IsRankOneDiscrete],
  Units.val '' ↑(Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator w)) = Set.range ⇑w \ {0}

Defined in: Mathlib.RingTheory.Valuation.Discrete.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrderedCommGroupWithZero Field Valuation.IsRankOneDiscrete

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
SetLike.coestatement and proof · cited by 8,199
Fieldstatement and proof · cited by 7,404
Set.imagestatement and proof · cited by 5,609
Set.rangestatement and proof · cited by 4,705
Subgroupstatement · cited by 3,593
Unitsstatement · cited by 2,804
Units.valstatement and proof · cited by 1,966
Valuationstatement and proof · cited by 823
LinearOrderedCommGroupWithZerostatement and proof · cited by 528
Subgroup.zpowersstatement · cited by 204

Cited by1

Results whose statement or proof uses this declaration.

Valuation.IsRankOneDiscrete.generator_mem_rangeproof · cited by 0