English
For hv = Integers v O, divisibility x | y in O is equivalent to v(algebraMap_O_F y) ≤ v(algebraMap_O_F x).
Русский
Для hv = Integers v O делимость x|y в O эквивалентна не большей или равной оценке v(y) ≤ v(x).
LaTeX
$$$x \\mid y \\;\\Longleftrightarrow\\; v(\\text{algebraMap}_{O,F}(y)) \\le v(\\text{algebraMap}_{O,F}(x))$$$
Lean4
theorem dvd_of_le (hv : Integers v O) {x y : O} (h : v (algebraMap O F x) ≤ v (algebraMap O F y)) : y ∣ x :=
by_cases
(fun hy : algebraMap O F y = 0 =>
have hx : x = 0 := hv.1 <| (algebraMap O F).map_zero.symm ▸ (v.zero_iff.1 <| le_zero_iff.1 (v.map_zero ▸ hy ▸ h))
hx.symm ▸ dvd_zero y)
fun hy : algebraMap O F y ≠ 0 =>
have : v ((algebraMap O F y)⁻¹ * algebraMap O F x) ≤ 1 :=
by
rw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul]
exact mul_le_mul_left' h _
let ⟨z, hz⟩ := hv.3 this
⟨z, hv.1 <| ((algebraMap O F).map_mul y z).symm ▸ hz.symm ▸ (mul_inv_cancel_left₀ hy _).symm⟩
