trace_prod — Mathlib

English

The trace map from R to S × T decomposes as the coproduct of traces to S and to T; i.e., Tr_{R}^{S×T} = Coprod(Tr_{R}^{S}, Tr_{R}^{T}).

Русский

След из R в S × T разлагается на копроизведение следов в S и в T: Tr_{R}^{S×T} = Coprod(Tr_{R}^{S}, Tr_{R}^{T}).

LaTeX

$$$\\operatorname{trace}_{R}^{S\\times T} = \\operatorname{coprod}(\\operatorname{trace}_{R}^{S}, \\operatorname{trace}_{R}^{T})$$$

Lean4

theorem trace_prod [Module.Free R S] [Module.Free R T] [Module.Finite R S] [Module.Finite R T] :
    trace R (S × T) = (trace R S).coprod (trace R T) :=
  LinearMap.ext fun p => by rw [coprod_apply, trace_prod_apply]

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