ext_hom — Mathlib

English

If two homomorphisms f,g: G →* H agree on the images of all basis elements b i, then f = g.

Русский

Если два гомоморфизма f,g: G →* H согласны на образы всех элементов базиса b i, то f = g.

LaTeX

$$(∀ i, f(b(i)) = g(b(i))) ⇒ f = g$$

Lean4

/-- If two morphisms on `G` coincide on the elements of a basis, then they coincide. -/
theorem ext_hom (b : FreeGroupBasis ι G) (f g : G →* H) (h : ∀ i, f (b i) = g (b i)) : f = g :=
  b.lift.symm.injective <| funext h

Похожие утверждения