Theorems · Theorem · ring theory

neg_one_mul

∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), -1 * a = -a

The additive inverse of one multiplied by an element of a ring is the element's additive inverse.

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

61 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

MulOneClassHasDistribNeg