Theorem Submodule.comap_covBy_of_surjective

Modification history

2025-12-27 09:40
Mathlib/LinearAlgebra/Span/Basic.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified Submodule.comap_covBy_of_surjectiveView on Github →
2025-04-04 14:05
Mathlib/LinearAlgebra/Span/Basic.lean
feat(RingTheory): lengths of modules (#23663)
Added Submodule.comap_covBy_of_surjectiveView on Github →