Commit 2024-02-20 23:51 89fd8bf0

View on Github →

feat: add lemma LinearMap.trace_restrict_eq_sum_trace_restrict (#10638)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

added theorem LinearMap.mapsTo_biSup_of_mapsTo

added theorem LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.isInternal_biSup_submodule_of_independent

Modified Mathlib/LinearAlgebra/Basic.lean

modified theorem LinearMap.ker_rangeRestrict

modified theorem LinearMap.range_rangeRestrict

added theorem LinearMap.surjective_rangeRestrict

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.biSup_comap_eq_top_of_range_eq_biSup

added theorem Submodule.biSup_comap_eq_top_of_surjective

added theorem Submodule.biSup_comap_subtype_eq_top

Modified Mathlib/Order/SupIndep.lean

added theorem CompleteLattice.independent_of_independent_coe_Iic_comp