chineseRemainderOfMultiset_lt_prod

English

The CRT remainder for a multiset is strictly less than the product of its mapped moduli.

Русский

Остаток CRT для мультсетa строго меньше произведения соответствующих модулей.

LaTeX

$$$\mathrm{chineseRemainderOfMultiset}\ a\ s\ nod\ hs\ pp < (m.map\ s).prod$$$

Lean4

theorem chineseRemainderOfMultiset_lt_prod {m : Multiset ι} (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0)
    (pp : Set.Pairwise {x | x ∈ m} (Coprime on s)) : chineseRemainderOfMultiset a s nod hs pp < (m.map s).prod :=
  by
  induction m using Quot.ind with
  | _ l
  unfold chineseRemainderOfMultiset
  simpa using chineseRemainderOfList_lt_prod a s l (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using hs)

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