existsUnique_equiv — Mathlib

English

For any a ∈ ℤ and b > 0, there exists z ∈ ℤ with 0 ≤ z < b and z ≡ a (mod b).

Русский

Пусть a ∈ ℤ и b > 0. Существует z ∈ ℤ такие, что 0 ≤ z < b и z ≡ a (mod b).

LaTeX

$$$\\forall a \\in \\mathbb{Z}, \\; \\forall b > 0, \\; \\exists z \\in \\mathbb{Z}, 0 \\le z < b \\land z \\equiv a [ZMOD b].$$$

Lean4

theorem existsUnique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
  ⟨a % b, emod_nonneg _ (ne_of_gt hb),
    by
    have : a % b < |b| := emod_lt_abs _ (ne_of_gt hb)
    rwa [abs_of_pos hb] at this, by simp [ModEq]⟩

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