dvd_total — Mathlib

English

In a valuation ring, any two elements x,y satisfy x|y or y|x (divisibility is total).

Русский

В валюационном кольце любой два элемента x,y удовлетворяют либо x делится на y, либо y делится на x.

LaTeX

$$$ x \\mid y \\lor y \\mid x $$$

Lean4

theorem dvd_total [Semigroup R] [h : PreValuationRing R] (x y : R) : x ∣ y ∨ y ∣ x :=
  @IsTotal.total _ _ (PreValuationRing.iff_dvd_total.mp h) x y

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