Theorems · Theorem · group theory

MulEquiv.ext

∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M ≃* N}, (∀ (x : M), f x = g x) → f = g

Two multiplicative isomorphisms agree if they are defined by the same underlying function.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

18 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

MulMul