map_trace — Mathlib

English

For any additive monoid hom f, f(tr(A)) = tr(A.map f).

Русский

Для любого аддитивного моноид-гомоморфа f выполняется f(tr(A)) = tr(A.map f).

LaTeX

$$$$ f( \operatorname{tr}(A) ) = \operatorname{tr}( A \mapsto f ) $$$$

Lean4

theorem _root_.AddMonoidHom.map_trace [AddCommMonoid S] {F : Type*} [FunLike F R S] [AddMonoidHomClass F R S] (f : F)
    (A : Matrix n n R) : f (trace A) = trace (A.map f) :=
  map_sum f (fun i => diag A i) Finset.univ

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