English
Permuting the indices in a list does not change the resulting Chinese remainder value when the moduli are permuted accordingly.
Русский
Перестановка списка не меняет получаемого остатка при соответствующей перестановке модулей.
LaTeX
$$$\mathrm{chineseRemainderOfList}\ a\ s\ l\ co = \mathrm{chineseRemainderOfList}\ a\ s\ l'\ (co.perm\ hl\ coprime\_comm.mpr)$$$
Lean4
theorem chineseRemainderOfList_perm {l l' : List ι} (hl : l.Perm l') (hs : ∀ i ∈ l, s i ≠ 0)
(co : l.Pairwise (Coprime on s)) :
(chineseRemainderOfList a s l co : ℕ) = chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr) :=
by
let z := chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr)
have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)
exact
(chineseRemainderOfList_modEq_unique a s l co (z := z)
(fun i hi => z.prop i (hl.symm.mem_iff.mpr hi))).symm.eq_of_lt_of_lt
(chineseRemainderOfList_lt_prod _ _ _ _ hs)
(by
rw [hlp]
exact chineseRemainderOfList_lt_prod _ _ _ _ (by simpa [List.Perm.mem_iff hl.symm] using hs))
