invFun_zero

Mathlib.RingTheory.MatrixAlgebra

URI: https://scilib.ai/kg/mathlib#MatrixEquivTensor.invFun_zero

English

The inverse functor sends the zero matrix to the zero tensor

Русский

Обратное отображение переводит нулевую матрицу в нулевой тензор

LaTeX

$$$ invFun\_n\,R\,A 0 = 0 $$$

Lean4

@[simp]
theorem invFun_zero : invFun n R A 0 = 0 := by simp [invFun]

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

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

Разделы

Аффилиация

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