det_mulLeft

Mathlib.LinearAlgebra.Determinant

URI: https://scilib.ai/kg/mathlib#LinearMap.det_mulLeft

English

For any a in the base ring R, the determinant of the left multiplication by a on R is a.

Русский

Для любого a в кольце R детерминант отображения левого умножения на a на R равен a.

LaTeX

$$$\det(\mathrm{mulLeft}\,R\ a) = a$$$

Lean4

theorem det_mulLeft (a : R) : (mulLeft R a).det = a := by simp

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

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

Разделы

Аффилиация

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