`BookProof.ChapterA.Jmap_mem_of_mem_JY` {Y : Submodule ℝ V} {x : V} (hx : x ∈ JY Y) : Jmap x ∈ Y

Initializing...

`BookProof.ChapterA.Jmap_mem_of_mem_JY` {Y : Submodule ℝ V} {x : V} (hx : x ∈ JY Y) : Jmap x ∈ Y · Prove2Me