A finite family in a ring with total divisibility has a member dividing all others

In a monoid with total divisibility, for instance a valuation ring or the p-adic integers, any two elements are comparable for divisibility. Consequently a finite nonempty family of elements has a member that divides every member of the family: the divisibility preorder restricted to the family is total, and a finite nonempty totally preordered set has a least element.

This is what picks, in a vector with entries in a discrete valuation ring, a coordinate of minimal valuation, which then divides all the other coordinates.

Main results

• TauCeti.PreValuationRing.exists_mem_forall_dvd: a finite nonempty family in a monoid with total divisibility has a member dividing every member.
• TauCeti.PreValuationRing.exists_forall_dvd: the same for a family indexed by a finite nonempty type.

theorem TauCeti.PreValuationRing.exists_mem_forall_dvd {R : Type u_1} [Monoid R] [PreValuationRing R] {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) (f : ι → R) : ∃ i ∈ s, ∀ j ∈ s, f i ∣ f j

In a monoid with total divisibility, a finite nonempty family has a member dividing every member of the family.

theorem TauCeti.PreValuationRing.exists_forall_dvd {R : Type u_1} [Monoid R] [PreValuationRing R] {ι : Type u_2} [Finite ι] [Nonempty ι] (f : ι → R) : ∃ (i : ι), ∀ (j : ι), f i ∣ f j

In a monoid with total divisibility, a family indexed by a finite nonempty type has a member dividing every member of the family.