English
Let f be a linear (or semilinear) map and let p ⊆ M be a submodule. Then p is disjoint from the kernel of f (i.e., p ∩ ker f = {0}) if and only if f is injective on p; equivalently, whenever x,y ∈ p satisfy f(x) = f(y), we must have x = y.
Русский
Пусть f — линейное (или полу-линейное) отображение, а p ⊆ M — подмодуля. Тогда p направляется в нулевой элемент ядра f эквивалентно тому, что ограничение f на p является инъективным; эквивалентно: если x,y ∈ p и f(x) = f(y), то x = y.
LaTeX
$$$\operatorname{Disjoint}(p, \ker f) \iff \forall x \in p, \forall y \in p, f\,x = f\,y \rightarrow x = y$$$
Lean4
theorem disjoint_ker' {p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y :=
disjoint_ker.trans
⟨fun H x hx y hy h => eq_of_sub_eq_zero <| H _ (sub_mem hx hy) (by simp [h]), fun H x h₁ h₂ =>
H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩
