instTrans

Mathlib.LinearAlgebra.SModEq

URI: https://scilib.ai/kg/mathlib#SModEq.instTrans

English

A transitive structure is instantiated for SModEq over a fixed U.

Русский

Для SModEq над фиксированным U существует инстанс транспозиции.

LaTeX

$$instance Trans (SModEq U) SModEq U SModEq U where trans := trans$$

Lean4

instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where trans := trans

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

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

Разделы

Аффилиация

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