R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    comp (comp (↑(Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
      ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))))
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(LinearEquiv.conj (Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0)
rw [LinearEquiv.conj_apply]
no goals
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    comp (comp (↑(Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
      ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))))
exact h.eq_conj_prod_map'