scale

Mathlib.Tactic.Linarith.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.Linexp.scale

Lean4

/-- `l.scale c` scales the values in `l` by `c` without modifying the order or keys. -/
def scale (c : Int) (l : Linexp) : Linexp :=
  if c = 0 then [] else if c = 1 then l else l.map fun ⟨n, z⟩ => (n, z * c)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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