norm_eq_matrix_det — Mathlib

English

For a finite index set ι with a basis b of S over R, the norm of s ∈ S equals the determinant of the matrix of left multiplication by s in that basis.

Русский

Для базиса b модуля S над R, размерность которого конечна, норма элемента s ∈ S равнаDet(матрица левого умножения на s в этом базисе).

LaTeX

$$$ \\operatorname{norm}_R(s) = \\det(\\mathrm{leftMulMatrix}_b(s)) $$$

Lean4

theorem norm_eq_matrix_det [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (s : S) :
    norm R s = Matrix.det (Algebra.leftMulMatrix b s) := by
  rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]; rfl

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