Commit 2025-07-12 02:16 33c4ca67

feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map (#22069) Added the lemma ne_map_or_ne_kernel_inter_of_lt stating that if A < B as submodules, then for any linear map f, ker f ⊓ A ≠ ker f ⊓ B ∨ Submodule.map f A ≠ Submodule.map f B. We also prove the corollaries ker_inter_mono_of_map_eq and map_mono_of_ker_inter_eq.