generator_mem_range — Mathlib

English

The image of the generator of w lies in the range of w.

Русский

Изображение генератора w принадлежит диапазону w.

LaTeX

$$$ \\uparrow(\\text{generator}(w)) \\in \\operatorname{range}(w). $$$

Lean4

theorem generator_mem_range (K : Type*) [Field K] (w : Valuation K Γ) [IsRankOneDiscrete w] :
    ↑(generator w) ∈ range w := by
  apply diff_subset
  rw [← generator_zpowers_eq_range]
  exact ⟨generator w, by simp⟩

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