subSquare

Mathlib.Tactic.Widget.CommDiag

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Widget.subSquare

Lean4

/-- Square with `homs = [f,g,h,i]` and `objs = [A,B,C,D]`
```
A f B
i   g
D h C
```
-/
def subSquare :=
  include_str ".." / ".." / ".." / "widget" / "src" / "penrose" / "square.sub"

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

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

Разделы

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

Аффилиация

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