Commit 2023-08-15 13:30 280a9f50

View on Github →

chore: golf some proofs introduced in #6360 (#6405) Notably, getting rid of some injectivity restrictions makes some later proofs simpler.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Free.lean

added def ModuleCat.Basis.ofShortExact

modified theorem ModuleCat.disjoint_span_sum

deleted theorem ModuleCat.family_injective_shortExact

modified theorem ModuleCat.span_rightExact

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

deleted theorem Submodule.ker_range_disjoint

added theorem Submodule.range_ker_disjoint