scalar

Mathlib.Tactic.Linarith.Parsing

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

Lean4

/-- A scalar `z` is represented by a `Sum` with coefficient `z` and monomial `one` -/
def scalar (z : ℤ) : Sum :=
  TreeMap.empty.insert one z

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

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

Разделы

Аффилиация

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