chineseRemainder — Mathlib

English

If n and m are coprime, there exists a unique k modulo nm such that k ≡ a mod n and k ≡ b mod m.

Русский

Если n и m взаимно простые, существует единственный k modulo nm такой, что k ≡ a (mod n) и k ≡ b (mod m).

LaTeX

$$$\\\\forall n,m\\\\in\\\\mathbb{N},\\\\ n \\\\perp m \\\\Rightarrow \\\\exists! k \\\\in \\\\mathbb{N},\\\\ k \\\\equiv a \\\\pmod{n} \\\\land \\\\ k \\\\equiv b \\\\pmod{m}$$$

Lean4

/-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
def chineseRemainder (co : n.Coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
  chineseRemainder' (by convert @modEq_one a b)

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