Commit 2023-07-14 11:52 1ce44f10

feat(LinearAlgebra.Span): add apply_mem_span_image_iff_mem_span (#5651) Add the other direction and iff version of submodule.apply_mem_span_image_of_mem_span, that is:

theorem apply_mem_span_image_iff_mem_span [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {x : M} {s : Set M} 
    (hf : Function.Injective f) :  f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s