ext — Mathlib

English

Two ring isomorphisms are equal if they agree on every element.

Русский

Две кольцевые изоморфные отображения равны, если они совпадают на каждом элементе.

LaTeX

$$ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g$$

Lean4

/-- Two ring isomorphisms agree if they are defined by the same underlying function. -/
@[ext]
theorem ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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