of_compatible_mulArchimedean — Mathlib

English

If Γ₀ is MulArchimedean and v is compatible, then ValuativeRel.IsRankLeOne R holds.

Русский

Если Γ₀ является MulArchimedean и v совместима, тогда ValuativeRel.IsRankLeOne R выполняется.

LaTeX

$$$[\mathrm{MulArchimedean}(\Gamma_0)](v) [v.Compatible] \Rightarrow \mathrm{ValuativeRel.IsRankLeOne\}R$$$

Lean4

theorem of_compatible_mulArchimedean [MulArchimedean Γ₀] (v : Valuation R Γ₀) [v.Compatible] :
    ValuativeRel.IsRankLeOne R := by
  rw [isRankLeOne_iff_mulArchimedean]
  exact .comap (ValueGroupWithZero.embed v).toMonoidHom (ValueGroupWithZero.embed_strictMono v)

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