R : Type u_1
R₁ : Type ?u.1255386
R₂ : Type u_2
R₃ : Type ?u.1255392
R₄ : Type ?u.1255395
S : Type ?u.1255398
K : Type ?u.1255401
K₂ : Type ?u.1255404
M : Type u_3
M' : Type ?u.1255410
M₁ : Type ?u.1255413
M₂ : Type u_4
M₃ : Type ?u.1255419
M₄ : Type ?u.1255422
N : Type ?u.1255425
N₂ : Type ?u.1255428
ι : Type ?u.1255431
V : Type ?u.1255434
V₂ : Type ?u.1255437
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.1255847
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0
R : Type u_1
R₁ : Type ?u.1255386
R₂ : Type u_2
R₃ : Type ?u.1255392
R₄ : Type ?u.1255395
S : Type ?u.1255398
K : Type ?u.1255401
K₂ : Type ?u.1255404
M : Type u_3
M' : Type ?u.1255410
M₁ : Type ?u.1255413
M₂ : Type u_4
M₃ : Type ?u.1255419
M₄ : Type ?u.1255422
N : Type ?u.1255425
N₂ : Type ?u.1255428
ι : Type ?u.1255431
V : Type ?u.1255434
V₂ : Type ?u.1255437
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.1255847
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range f ≤ ⊥ ↔ f = 0
rw [range_le_iff_comap]
no goals
R : Type u_1
R₁ : Type ?u.1255386
R₂ : Type u_2
R₃ : Type ?u.1255392
R₄ : Type ?u.1255395
S : Type ?u.1255398
K : Type ?u.1255401
K₂ : Type ?u.1255404
M : Type u_3
M' : Type ?u.1255410
M₁ : Type ?u.1255413
M₂ : Type u_4
M₃ : Type ?u.1255419
M₄ : Type ?u.1255422
N : Type ?u.1255425
N₂ : Type ?u.1255428
ι : Type ?u.1255431
V : Type ?u.1255434
V₂ : Type ?u.1255437
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.1255847
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0
exact ker_eq_top