existsUnique_equiv_nat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem existsUnique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
  let ⟨z, hz1, hz2, hz3⟩ := existsUnique_equiv a hb
  ⟨z.natAbs, by constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption⟩

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