English
Another formal variant stating L ∩ ker f = {0} under a finrank inequality.
Русский
Ещё одна формальная разновидность: пересечение тривиально при условии рангов.
LaTeX
$$$L \cap \ker f = \{0\}$ under the stated finrank inequality.$$
Lean4
theorem disjoint_ker_of_finrank_le [NoZeroSMulDivisors R M] {N : Type*} [AddCommGroup N] [Module R N]
{L : Submodule R M} [Module.Finite R L] (f : M →ₗ[R] N) (h : finrank R L ≤ finrank R (L.map f)) :
Disjoint L (LinearMap.ker f) :=
by
refine
disjoint_iff.mpr <|
LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <| Submodule.rank_eq_zero.mp ?_
rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]
rw [← LinearMap.range_domRestrict] at h
have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank
rw [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange] at this
omega
