Theorems · Theorem · commutative algebra

Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange

∀ {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O F] {v : Valuation F Γ₀} [Nontrivial (↥(MonoidHom.mrange v))ˣ],
  v.Integers O →
    (WellFounded (Function.onFun (fun x1 x2 => x1 > x2) (⇑v ∘ ⇑(algebraMap O F))) ↔
      Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ)))

Defined in

Mathlib.RingTheory.Valuation.Archimedean

Cited by

1 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderedCommGroupWithZeroCommRingAlgebraNontrivial