English
For x,y in O, DvdNotUnit x y holds exactly when v(φ(y)) < v(φ(x)).
Русский
Для элементов x,y ∈ O выполняется DvdNotUnit x y тогда и только тогда, когда v(φ(y)) < v(φ(x)).
LaTeX
$$$\mathrm{DvdNotUnit}(x,y) \iff v(\mathrm{algebraMap}(O,F)(y)) < v(\mathrm{algebraMap}(O,F)(x))$$$
Lean4
theorem dvdNotUnit_iff_lt (hv : Integers v O) {x y : O} :
DvdNotUnit x y ↔ v (algebraMap O F y) < v (algebraMap O F x) :=
by
rw [lt_iff_le_not_ge, hv.le_iff_dvd, hv.le_iff_dvd]
refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩
rintro ⟨hx0, d, hdu, rfl⟩
refine ⟨⟨d, rfl⟩, ?_⟩
rw [hv.isUnit_iff_valuation_eq_one, ← ne_eq, ne_iff_lt_iff_le.mpr (hv.map_le_one d)] at hdu
rw [dvd_iff_le hv]
simp only [map_mul, not_le]
contrapose! hdu
refine one_le_of_le_mul_left₀ ?_ hdu
simp [hv.valuation_pos_iff_ne_zero, hx0]
