dvd_of_toWithBotNat_le_toWithBotNat

English

If x ≠ 0 and the valuation of x is less than or equal to that of y in a DVR, then x divides y.

Русский

Если x ≠ 0 и v(x) ≤ v(y) в дискретном оценочном кольце, то x делит y.

LaTeX

$$$\\mathrm{toWithBotNat}(x) \\le \\mathrm{toWithBotNat}(y) \\Rightarrow x \\mid y \\quad (x \\neq 0)$$$

Lean4

theorem dvd_of_toWithBotNat_le_toWithBotNat (x y : R) (hx : x ≠ 0) (hle : toWithBotNat x ≤ toWithBotNat y) : x ∣ y :=
  by
  by_cases hy : y = 0
  · simp [hy, hx] at hle
  exact (toWithBotNat_le_toWithBotNat_iff hx hy).mp hle

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