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

@[instance_reducible]

instance MonoidWithZeroHom.instLinearOrderedCommGroupWithZeroMrange {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : F →*₀ Γ₀) : LinearOrderedCommGroupWithZero ↥(MonoidHom.mrange v)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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 ↥(MonoidHom.mrange v)] (hv : v.Integers O) : IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↑(Set.range ⇑v)

theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O F] {v : Valuation F Γ₀} [MulArchimedean ↥(MonoidHom.mrange v)] (hv : v.Integers O) : IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↥(MonoidHom.mrange v)