dvd_iff_le — Mathlib

English

A variant of the le_of_dvd lemma asserts that if x|y then v(algebraMap y) ≤ v(algebraMap x).

Русский

Вариант леммы le_of_dvd утверждает, что если x делит y, то v(y)≤v(x).

LaTeX

$$$\\text{Let's denote: } \\text{le_of_dvd}(hv, x, y, h) : v(\\text{algebraMap}_{O,F}(y)) \\le v(\\text{algebraMap}_{O,F}(x))$$$

Lean4

theorem dvd_iff_le (hv : Integers v O) {x y : O} : x ∣ y ↔ v (algebraMap O F y) ≤ v (algebraMap O F x) :=
  ⟨hv.le_of_dvd, hv.dvd_of_le⟩

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