Ring of integers under a given valuation in an multiplicatively archimedean codomain

instance instLinearOrderedCommGroupWithZeroSubtypeMemSubmonoidMrangeValuation {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} : LinearOrderedCommGroupWithZero ↥(MonoidHom.mrange v)

Equations

• instLinearOrderedCommGroupWithZeroSubtypeMemSubmonoidMrangeValuation = LinearOrderedCommGroupWithZero.mk ⋯ CommGroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

theorem Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O F] {v : Valuation F Γ₀} (hv : v.Integers O) : WfDvdMonoid O ↔ WellFounded (Function.onFun (fun (x1 x2 : Γ₀) => x1 > x2) (⇑v ∘ ⇑(algebraMap O F)))

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

theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O F] {v : Valuation F Γ₀} [MulArchimedean Γ₀] (hv : v.Integers O) : IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↑(Set.range ⇑v)