det_toLin'

Mathlib.LinearAlgebra.Determinant

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

English

If f is a matrix, then the determinant of the linear map toLin under basis b equals the determinant of f.

Русский

Если f — матрица, тоDet( toLin b b f ) = det f.

LaTeX

$$$\det(\mathrm{toLin}\, b\, b\, f) = \det f$$$

Lean4

@[simp]
theorem det_toLin' (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin' f) = Matrix.det f := by
  simp only [← toLin_eq_toLin', det_toLin]

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

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

Разделы

Аффилиация

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