English
The graph of the inverse is the graph of f with coordinates swapped, i.e., f.graph mapped by prodComm.
Русский
Граф обратного — график f с обменом координат, то есть граф f отображается путем prodComm.
LaTeX
$$(f.inverse).graph = f.graph.map (LinearEquiv.prodComm R E F)$$
Lean4
/-- The graph of the inverse generates a `LinearPMap`. -/
theorem mem_inverse_graph_snd_eq_zero (x : F × E) (hv : x ∈ (graph f).map (LinearEquiv.prodComm R E F))
(hv' : x.fst = 0) : x.snd = 0 :=
by
simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk] at hv
rcases hv with ⟨a, b, ⟨ha, h1⟩, ⟨h2, h3⟩⟩
simp only at hv' ⊢
rw [hv'] at h1
rw [LinearMap.ker_eq_bot'] at hf
specialize hf ⟨a, ha⟩ h1
simp only [Submodule.mk_eq_zero] at hf
exact hf
