Theorems · Theorem · group theory

AddEquiv.ext

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

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

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

30 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

AddAdd