R : Type u_2
R₁ : Type ?u.1232780
R₂ : Type u_1
R₃ : Type ?u.1232786
R₄ : Type ?u.1232789
S : Type ?u.1232792
K : Type ?u.1232795
K₂ : Type ?u.1232798
M : Type u_3
M' : Type ?u.1232804
M₁ : Type ?u.1232807
M₂ : Type u_4
M₃ : Type ?u.1232813
M₄ : Type ?u.1232816
N : Type ?u.1232819
N₂ : Type ?u.1232822
ι : Type ?u.1232825
V : Type ?u.1232828
V₂ : Type ?u.1232831
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type ?u.1233241
sc : SemilinearMapClass F τ₁₂ M M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
⊢ comap f ⊥ = ker f
R : Type u_2
R₁ : Type ?u.1232780
R₂ : Type u_1
R₃ : Type ?u.1232786
R₄ : Type ?u.1232789
S : Type ?u.1232792
K : Type ?u.1232795
K₂ : Type ?u.1232798
M : Type u_3
M' : Type ?u.1232804
M₁ : Type ?u.1232807
M₂ : Type u_4
M₃ : Type ?u.1232813
M₄ : Type ?u.1232816
N : Type ?u.1232819
N₂ : Type ?u.1232822
ι : Type ?u.1232825
V : Type ?u.1232828
V₂ : Type ?u.1232831
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type ?u.1233241
sc : SemilinearMapClass F τ₁₂ M M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
⊢ ker (codRestrict p f hf) = ker f
rw [ker, comap_codRestrict, Submodule.map_bot]
no goals
R : Type u_2
R₁ : Type ?u.1232780
R₂ : Type u_1
R₃ : Type ?u.1232786
R₄ : Type ?u.1232789
S : Type ?u.1232792
K : Type ?u.1232795
K₂ : Type ?u.1232798
M : Type u_3
M' : Type ?u.1232804
M₁ : Type ?u.1232807
M₂ : Type u_4
M₃ : Type ?u.1232813
M₄ : Type ?u.1232816
N : Type ?u.1232819
N₂ : Type ?u.1232822
ι : Type ?u.1232825
V : Type ?u.1232828
V₂ : Type ?u.1232831
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type ?u.1233241
sc : SemilinearMapClass F τ₁₂ M M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
⊢ comap f ⊥ = ker f
rfl