generator — Mathlib

English

Equality between zpowers of the generator and the value group: zpowers(generator v) = valueGroup v.

Русский

Равенство: zpowers(generator v) = valueGroup(v).

LaTeX

$$$ \\operatorname{zpowers}(\\operatorname{generator}(v)) = \\operatorname{valueGroup}(v). $$$

Lean4

/-- Given a discrete valuation `v`, `Valuation.IsRankOneDiscrete.generator` is a generator of
the value group that is `< 1`. -/
noncomputable def generator : Γˣ :=
  (exists_generator_lt_one v).choose

Похожие утверждения