det_one_smulRight — Mathlib

English

For any v in the base ring 𝕜, the determinant of the endomorphism of 𝕜 given by right multiplication by v equals v.

Русский

Для любого v в осн. кольце 𝕜 определитель эндоморфизма 𝕜, заданного правым умножением на v, равен v.

LaTeX

$$$\det\bigl((1 : 𝕜 \to_L[𝕜] 𝕜).smulRight v\bigr) = v$$$

Lean4

theorem det_one_smulRight {𝕜 : Type*} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) :
    ((1 : 𝕜 →L[𝕜] 𝕜).smulRight v).det = v := by simp

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