Theorem Submodule.biSup_comap_eq_top_of_surjective

Modification history

2024-02-20 23:51
Mathlib/LinearAlgebra/Span.lean
feat: add lemma `LinearMap.trace_restrict_eq_sum_trace_restrict` (#10638)
Added Submodule.biSup_comap_eq_top_of_surjectiveView on Github →