theorem LinearEquiv.map_coe {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (U : Submodule R M₁) : Submodule.map (↑e) U = Submodule.map e U

@[simp]

theorem LinearEquiv.map_trans {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (e₁₂ : M₁ ≃ₗ[R] M₂) (e₂₃ : M₂ ≃ₗ[R] M₃) (U : Submodule R M₁) : Submodule.map (e₁₂ ≪≫ₗ e₂₃) U = Submodule.map e₂₃ (Submodule.map e₁₂ U)

theorem Submodule.mem_span_singleton₀ {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommMonoid M] [Module R M] {x y : M} (hx : x ≠ 0) : x ∈ span R {y} ↔ ∃ (a : Rˣ), a • y = x