ext — Mathlib

English

Two homomorphisms from a presented group to a group G are equal if they agree on all generators.

Русский

Два гомоморфизма из презентации в группу совпадают, если они совпадают на всех генераторах.

LaTeX

$$ext {φ ψ : PresentedGroup rels →* G} (hx : ∀ x, φ(of x) = ψ(of x)) : φ = ψ$$

Lean4

@[ext]
theorem ext {φ ψ : PresentedGroup rels →* G} (hx : ∀ (x : α), φ (.of x) = ψ (.of x)) : φ = ψ :=
  by
  unfold PresentedGroup
  ext
  apply hx

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