ext — Mathlib

English

Any order ring iso composed with its inverse yields the identity iso.

Русский

Любой упорядоченный кольцевой изоморфизм, составленный с обратным, даёт тождественный изоморфизм.

LaTeX

$$$\forall e:\alpha \overset{\text{OrderRingIso}}{\cong} \beta,\; e.\texttrans e^{-1} = \mathrm{refl}$$$

Lean4

@[ext]
theorem ext {f g : α ≃+*o β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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