instCommGroupWithZeroSubtypeMemSubmonoidMrange

English

For a discrete valuation v, there exists a unit γ of Γ such that zpowers(γ) = valueGroup(v).

Русский

Для дискретной валюации v существует единичный элемент γ группы Γ такой, что zpowers(γ) = valueGroup(v).

LaTeX

$$$ \\exists \\gamma \\in \\Gamma^{\\times},\\ \\operatorname{zpowers}(\\gamma) = \\operatorname{valueGroup}(v). $$$

Lean4

instance {Γ₀} [LinearOrderedCommGroupWithZero Γ₀] [DivisionRing K] (v : Valuation K Γ₀) :
    CommGroupWithZero (MonoidHom.mrange v) :=
  inferInstanceAs (CommGroupWithZero (MonoidHom.mrange (v : K →*₀ Γ₀)))

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