instMulArchimedeanValueGroupWithZeroOfIsRankLeOne

English

Any rank-at-most-one valuation has a mul-archimedean value group; in particular, ValueGroupWithZero R is MulArchimedean under IsRankLeOne R.

Русский

Любая валюация ранга не более единицы имеет mul-архимедову группу значений; ValueGroupWithZero R является MulArchimedean при IsRankLeOne R.

LaTeX

$$$\\text{MulArchimedean}(\\mathrm{ValueGroupWithZero} R)$$$

Lean4

/-- Any rank-at-most-one valuation has a mul-archimedean value group.
The converse (for any compatible valuation) is `ValuativeRel.isRankLeOne_iff_mulArchimedean`
which is in a later file since it requires a larger theory of reals. -/
instance [IsRankLeOne R] : MulArchimedean (ValueGroupWithZero R) :=
  by
  obtain ⟨⟨f, hf⟩⟩ := IsRankLeOne.nonempty (R := R)
  exact .comap f.toMonoidHom hf

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