toString

Mathlib.Tactic.Positivity.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.Strictness.toString

Lean4

/-- Gives a generic description of the `positivity` result. -/
def toString {e : Q($α)} : Strictness zα pα e → String
  | positive _ => "positive"
  | nonnegative _ => "nonnegative"
  | nonzero _ => "nonzero"
  | none => "none"

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

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

Разделы

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

Аффилиация

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