Commit 2023-11-24 12:19 7efcade4

View on Github →

feat: various linear algebra results (#8572)

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

added theorem LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

added theorem LinearMap.restrict_commute

added theorem LinearMap.restrict_comp

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added def LinearMap.extendScalars

added theorem LinearMap.extendScalars_comp

added theorem LinearMap.extendScalars_tmul

added def Submodule.extendScalars

added theorem Submodule.extendScalars_bot

added theorem Submodule.extendScalars_span

added theorem Submodule.extendScalars_top

added theorem Submodule.tmul_mem_extendScalars_of_mem

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_extendScalars

Modified Mathlib/Logic/Basic.lean

added theorem exists_exists_and_exists_and_eq_and

Modified Mathlib/RingTheory/TensorProduct.lean

added theorem Algebra.TensorProduct.basis_apply

added theorem LinearMap.toMatrix_extendScalars