_example

Mathlib.LinearAlgebra.Matrix.ToLin

URI: https://scilib.ai/kg/mathlib#_example

Lean4

example {A} [Semiring A] [Fintype m] :=
  (vecMulBilin A Aᵐᵒᵖ : _ →ₗ[_] Matrix m n A →ₗ[_] _)

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

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

Разделы

Аффилиация

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