English
Let V be a finite-dimensional vector space over a field K. If f,g are linear functionals on V (i.e., elements of V*), and there exists x in V such that ker f = ker g, f(x) = g(x), and f(x) ≠ 0, then f = g.
Русский
Пусть V — конечномерное векторное пространство над полем K. Пусть f и g — линейные функционалы на V (элементы V*). Если существует x ∈ V такое, что ker f = ker g, f(x) = g(x) и f(x) ≠ 0, то f = g.
LaTeX
$$$\\forall V\\, [\\text{FiniteDimensional}_K V],\\; \\forall f,g \\in V^*,\\; \\forall x \\in V,\\ ker f = ker g \\land f(x) = g(x) \\land f(x) \\neq 0 \\Rightarrow f = g$$$
Lean4
theorem eq_of_ker_eq_of_apply_eq [FiniteDimensional K V₁] {f g : Module.Dual K V₁} (x : V₁)
(h : LinearMap.ker f = LinearMap.ker g) (h' : f x = g x) (hx : f x ≠ 0) : f = g :=
by
let p := K ∙ x
have hp : p ≠ ⊥ := by aesop
have hpf : Disjoint (LinearMap.ker f) p :=
by
rw [disjoint_iff, Submodule.eq_bot_iff]
rintro y ⟨hfy : f y = 0, hpy : y ∈ p⟩
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy
have ht : t = 0 := by simpa [hx] using hfy
simp [ht]
have hf : f ≠ 0 := by aesop
ext v
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ᵉ (y ∈ LinearMap.ker f) (z ∈ p), y + z = v :=
by
have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this
have hy' : g y = 0 := by rwa [← LinearMap.mem_ker, ← h]
replace hy : f y = 0 := by rwa [LinearMap.mem_ker] at hy
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hz
simp [h', hy, hy']
