trace_one — Mathlib

English

The trace of the identity endomorphism on a finite free module equals its dimension (rank).

Русский

След тождественного отображения на конечном свободном модуле равен его размерности (рангу).

LaTeX

$$$ \operatorname{trace}_R M \; id = \operatorname{finrank}_R M. $$$

Lean4

/-- The trace of the identity endomorphism is the dimension of the free module. -/
@[simp]
theorem trace_one : trace R M 1 = (finrank R M : R) :=
  by
  cases subsingleton_or_nontrivial R
  · simp [eq_iff_true_of_subsingleton]
  have b := Module.Free.chooseBasis R M
  rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
  simp

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