det_ring — Mathlib

English

For a linear map f from a commutative ring R to itself, the determinant equals the value at 1: det f = f(1).

Русский

Для линейного отображения f над кольцом R детерминант равен значению в 1: det f = f(1).

LaTeX

$$$\det f = f(1)$$$

Lean4

/-- When the function is over the base ring, the determinant is the evaluation at `1`. -/
@[simp]
theorem det_ring (f : R →ₗ[R] R) : f.det = f 1 := by simp [← det_toMatrix (Basis.singleton Unit R)]

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