trace_id — Mathlib

English

Equivalently, the trace of the identity endomorphism equals the rank of the module.

Русский

Эквивалентно, след тождественного отображения равен ранку модуля.

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_id : trace R M id = (finrank R M : R) := by rw [← Module.End.one_eq_id, trace_one]

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