ext — Mathlib

English

A multiplicative equivalence equals its underlying equiv when viewed as an equivalence.

Русский

Мультиэквивалент равен своей подлежащей эквивалентности, если рассматривать его как эквивалентность.

LaTeX

$$$$f^{toEquiv} = f.$$$$

Lean4

/-- Two multiplicative isomorphisms agree if they are defined by the
same underlying function. -/
@[to_additive (attr := ext) /-- Two additive isomorphisms agree if they are defined by the same underlying function. -/
    ]
theorem ext {f g : MulEquiv M N} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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