toWithBotNat_le_toWithBotNat_iff — Mathlib

English

Let R be a discrete valuation ring. For nonzero x,y, we have toWithBotNat x ≤ toWithBotNat y if and only if x divides y.

Русский

Пусть R — дискретное оценочное кольцо. Для ненулевых x,y верно: v(x) ≤ v(y) тогда и только тогда, когда x делится на y.

LaTeX

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

Lean4

theorem toWithBotNat_le_toWithBotNat_iff {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    toWithBotNat x ≤ toWithBotNat y ↔ x ∣ y := by
  unfold toWithBotNat
  generalize hvx : addVal R x = vx
  generalize hvy : addVal R y = vy
  cases vx with
  | top => rw [addVal_eq_top_iff] at hvx; tauto
  | coe vx =>
    cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

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