Mathlib Changelog
v4
Changelog
About
Github
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