Theorem: LinearMap.ker_baseChange_of_linearProjOfIsCompl (DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean)

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ ker (baseChange R (M₁.linearProjOfIsCompl M₂ hM)) = range (baseChange R M₂.subtype)
Tactic:
simpa only [← exact_iff] using ker_lTensor_of_linearProjOfIsCompl hM R
State after:
no goals