no goals
R : Type u_1
R₁ : Type ?u.1371370
R₂ : Type u_3
R₃ : Type ?u.1371376
R₄ : Type ?u.1371379
S : Type ?u.1371382
K : Type ?u.1371385
K₂ : Type ?u.1371388
M : Type u_2
M' : Type ?u.1371394
M₁ : Type ?u.1371397
M₂ : Type u_4
M₃ : Type ?u.1371403
M₄ : Type ?u.1371406
N : Type ?u.1371409
N₂ : Type ?u.1371412
ι : Type ?u.1371415
V : Type ?u.1371418
V₂ : Type ?u.1371421
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
H : ∀ (x : M), x ∈ p → ↑f x = 0 → x = 0
x : M
hx : x ∈ p
y : M
hy : y ∈ p
h : ↑f x = ↑f y
⊢ ↑f (x - y) = 0
simp [h]
no goals
R : Type u_1
R₁ : Type ?u.1371370
R₂ : Type u_3
R₃ : Type ?u.1371376
R₄ : Type ?u.1371379
S : Type ?u.1371382
K : Type ?u.1371385
K₂ : Type ?u.1371388
M : Type u_2
M' : Type ?u.1371394
M₁ : Type ?u.1371397
M₂ : Type u_4
M₃ : Type ?u.1371403
M₄ : Type ?u.1371406
N : Type ?u.1371409
N₂ : Type ?u.1371412
ι : Type ?u.1371415
V : Type ?u.1371418
V₂ : Type ?u.1371421
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
H : ∀ (x : M), x ∈ p → ∀ (y : M), y ∈ p → ↑f x = ↑f y → x = y
x : M
h₁ : x ∈ p
h₂ : ↑f x = 0
⊢ ↑f x = ↑f 0
simpa using h₂