wfDvdMonoid_iff_wellFounded_gt_on_v

English

For a valuation v with integers, the well-foundedness of the order '>' on v ∘ algebraMap O F is equivalent to the existence of a nontrivial isomorphism between the Monoid range of v and the integers, under discreteness conditions.

Русский

Для оценки v с целыми числами равенство: хорошо упорядованность отношения '>' на v ∘ algebraMap O F эквивалентна существованию ненулевого изоморфизма между образами v и целыми числами при условии дискретности.

LaTeX

$$$\\mathrm{WfDvdMonoid}(O) \\iff \\mathrm{WellFounded}((\\cdot > \\cdot) \\text{ on } (v \\circ \\mathrm{algebraMap}\\; O\\; F)).$$$

Lean4

theorem wfDvdMonoid_iff_wellFounded_gt_on_v (hv : Integers v O) :
    WfDvdMonoid O ↔ WellFounded ((· > ·) on (v ∘ algebraMap O F)) := by
  refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩ <;> simp [Function.onFun, hv.dvdNotUnit_iff_lt]

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