ext — Mathlib

English

If two nonunital star ring homomorphisms f and g agree on all elements of their domain, then f = g.

Русский

Если два отображения, сохраняющие структуру звезды и несуществование единицы, совпадают на каждом элементе области определения, то они равны.

LaTeX

$$$$\\forall x,\\ f(x)=g(x) \\implies f=g.$$$$

Lean4

@[ext]
theorem ext {f g : A →⋆ₙ+* B} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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