English
Given a finite multiset of indices with nonzero s-values and pairwise Coprime on s, the Chinese remainder value is less than the product of s-values mapped over the multiset.
Русский
Для мультимножества индексов с ненулевыми s-значеними и попарной взаимно простотой относительно s, остаток Чайнeс-остатка меньше произведения s.
LaTeX
$$$\mathrm{chineseRemainderOfMultiset}\ a\ s\ m \ nod\ hs\ pp < (m.map\ s).prod$$$
Lean4
/-- The natural number less than `(m.map s).prod` congruent to
`a i` mod `s i` for all `i ∈ m`. -/
def chineseRemainderOfMultiset {m : Multiset ι} :
m.Nodup → (∀ i ∈ m, s i ≠ 0) → Set.Pairwise {x | x ∈ m} (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] } :=
Quotient.recOn m (fun l nod _ co => chineseRemainderOfList a s l (List.Nodup.pairwise_of_forall_ne nod co))
(fun l l' (pp : l.Perm l') ↦
funext fun nod' : l'.Nodup =>
have nod : l.Nodup := pp.symm.nodup_iff.mp nod'
funext fun hs' : ∀ i ∈ l', s i ≠ 0 =>
have hs : ∀ i ∈ l, s i ≠ 0 := by simpa [List.Perm.mem_iff pp] using hs'
funext fun co' : Set.Pairwise {x | x ∈ l'} (Coprime on s) =>
have co : Set.Pairwise {x | x ∈ l} (Coprime on s) := by simpa [List.Perm.mem_iff pp] using co'
have lco : l.Pairwise (Coprime on s) := List.Nodup.pairwise_of_forall_ne nod co
have :
∀ {m' e nod'' hs'' co''},
@Eq.ndrec (Multiset ι) l
(fun m ↦
m.Nodup →
(∀ i ∈ m, s i ≠ 0) →
Set.Pairwise {x | x ∈ m} (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
(fun nod _ co ↦ chineseRemainderOfList a s l (List.Nodup.pairwise_of_forall_ne nod co)) m' e nod''
hs'' co'' =
(chineseRemainderOfList a s l lco : ℕ) :=
by rintro _ rfl _ _ _; rfl
by ext; exact this.trans <| chineseRemainderOfList_perm a s pp hs lco)
