chineseRemainderOfList_nil

Mathlib.Data.Nat.ChineseRemainder

URI: https://scilib.ai/kg/mathlib#Nat.chineseRemainderOfList_nil

English

For the empty list, the remainder is 0.

Русский

Для пустого списка остаток равен 0.

LaTeX

$$$\mathrm{chineseRemainderOfList\ } a\ s\ List.nil\ List.Pairwise.nil = 0$$$

Lean4

@[simp]
theorem chineseRemainderOfList_nil : (chineseRemainderOfList a s [] List.Pairwise.nil : ℕ) = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru