det_mulRight

Mathlib.LinearAlgebra.Determinant

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

English

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

Русский

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

LaTeX

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

Lean4

theorem det_mulRight (a : R) : (mulRight R a).det = a := by simp

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

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

Разделы

Аффилиация

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