Theorems · Theorem · linear algebra

LinearMap.trace_eq_sum_trace_restrict

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)]
  [∀ (i : ι), Module.Free R ↥(N i)],
  DirectSum.IsInternal N →
    ∀ [inst_6 : Fintype ι] {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)),
      (LinearMap.trace R M) f = ∑ i, (LinearMap.trace R ↥(N i)) (f.restrict ⋯)

The trace of an endomorphism of a direct sum is the sum of the traces on each component. See also LinearMap.trace_restrict_eq_sum_trace_restrict.

Defined in

Mathlib.Algebra.DirectSum.LinearMap

Cited by

3 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleDecidableEqModule.FiniteModule.FreeFintype