toMatrix'_apply

Mathlib.LinearAlgebra.Matrix.ToLin

URI: https://scilib.ai/kg/mathlib#LinearMap.toMatrix'_apply

← MathLib Explorer

English

The inverse of toLin' equals toMatrix'.symm.

Русский

Обратная к toLin' равна toMatrix'.symm.

LaTeX

$$theorem toLin'_symm : (Matrix.toLin'.symm : ((n → R) →ₗ[R] m → R) ≃ₗ[R] _) = LinearMap.toMatrix'$$

Lean4

@[simp]
theorem toMatrix'_apply (f : (n → R) →ₗ[R] m → R) (i j) :
    LinearMap.toMatrix' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by simp [toMatrix', ← Pi.single_apply]

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

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

Разделы

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

Аффилиация

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