Theorems · Theorem · group theory

AddEquiv.map_neg

∀ {G : Type u_7} {H : Type u_8} [inst : AddGroup G] [inst_1 : SubtractionMonoid H] (h : G ≃+ H) (x : G), h (-x) = -h x

An additive equivalence of additive groups preserves negation.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

9 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

AddGroupSubtractionMonoid