Commit 2023-11-16 10:23 0e1fb8d5

View on Github →

feat: the trace of a direct sum is the sum of the traces (#8369)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/LinearMap.lean

added theorem LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal'

added theorem LinearMap.trace_eq_sum_trace_restrict

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.IsInternal.collectedBasis_repr_of_mem

added theorem DirectSum.IsInternal.collectedBasis_repr_of_mem_ne

added theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem

added theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne

added theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne

added theorem DirectSum.IsInternal.ofBijective_coeLinearMap_same

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.Finite.coeSort_toFinset

added def Set.Finite.subtypeEquivToFinset

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem LinearEquiv.ofBijective_symm_apply_apply

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

added theorem Matrix.trace_blockDiagonal'

added theorem Matrix.trace_blockDiagonal

Modified Mathlib/Order/CompactlyGenerated.lean

added theorem CompleteLattice.WellFounded.finite_ne_bot_of_independent

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/SupIndep.lean

added theorem CompleteLattice.independent_ne_bot_iff_independent

Modified Mathlib/RingTheory/Noetherian.lean

added theorem Submodule.finite_ne_bot_of_independent