mul

Mathlib.Data.Num.Bitwise

URI: https://scilib.ai/kg/mathlib#SNum.mul

Lean4

/-- Multiply two `SNum`s. -/
protected def mul (a : SNum) : SNum → SNum :=
  rec' (fun b ↦ cond b (-a) 0) fun b _ IH ↦ cond b (bit0 IH + a) (bit0 IH)

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

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

Разделы

Аффилиация

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