instToMessageDataProjectionData

Mathlib.Tactic.Simps.Basic

URI: https://scilib.ai/kg/mathlib#Simps.instToMessageDataProjectionData

Lean4

instance : ToMessageData ProjectionData where
  toMessageData
    | ⟨a, b, c, d, e⟩ =>
      .group <|
        .nest 1 <|
          "⟨" ++
              .joinSep [toMessageData a, toMessageData b, toMessageData c, toMessageData d, toMessageData e]
                ("," ++ Format.line) ++
            "⟩"

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

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

Разделы

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

Аффилиация

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