traceAddMonoidHom — Mathlib

English

The map A ↦ tr(A) is an additive monoid hom from matrices to the underlying additive monoid R.

Русский

Отображение A ↦ tr(A) является аддитивным моноид-гомоморфизмом из матриц в R.

LaTeX

$$$$ \text{tr}(0) = 0 \quad \text{и} \quad \operatorname{tr}(A) + \operatorname{tr}(B) = \operatorname{tr}(A + B) $$$$

Lean4

/-- `Matrix.trace` as an `AddMonoidHom` -/
@[simps]
def traceAddMonoidHom : Matrix n n R →+ R where
  toFun := trace
  map_zero' := trace_zero n R
  map_add' := trace_add

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