instRepr

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.instRepr

Lean4

/-- The `Repr` instance converts terms to strings in a way that
reflects the matrix/vector interpretation as above. -/
instance : Repr XgcdType where
  reprPrec
    | g, _ =>
      s!"[[[{(repr (g.wp + 1))}, {(repr g.x)}], \
                         [{(repr g.y)}, {(repr (g.zp + 1))}]], \
                        [{(repr (g.ap + 1))}, {repr (g.bp + 1)}]]"

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

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

Разделы

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

Аффилиация

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