English
If hf is an EssFiniteType witness for f, and g1,g2: S → T satisfy g1 ∘ f = g2 ∘ f and agree on the finite set hf.finset, then g1 = g2.
Русский
Если hf является свидетелем EssFiniteType для f, и g1,g2: S → T удовлетворяют g1 ∘ f = g2 ∘ f и совпадают на конечном наборе hf.finset, то g1 = g2.
LaTeX
$$$\forall f:\,R\to S,\ hf: f.EssFiniteType,\forall g_1,g_2:\,S\to T,\ (g_1\circ f = g_2\circ f) \to (\forall x\in hf.finset,\; g_1(x)=g_2(x)) \Rightarrow g_1=g_2$$$
Lean4
theorem ext (hf : f.EssFiniteType) {g₁ g₂ : S →+* T} (h₁ : g₁.comp f = g₂.comp f) (h₂ : ∀ x ∈ hf.finset, g₁ x = g₂ x) :
g₁ = g₂ := by
algebraize [f, g₁.comp f]
ext x
exact DFunLike.congr_fun (Algebra.EssFiniteType.algHom_ext T ⟨g₁, fun _ ↦ rfl⟩ ⟨g₂, DFunLike.congr_fun h₁.symm⟩ h₂) x
