Mathlib Map

Theorems · Definition · group theory

AddUnits.neg

{α : Type u} → [inst : AddMonoid α] → AddUnits α → α

The additive inverse value of val in the base AddMonoid.

Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
14 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddUnits.map · cited by 16AddUnits.mapAddEquiv.piAddUnits · cited by 5AddEquiv.piAddUnitsAddUnits.mulLeft · cited by 5AddUnits.mulLeftAddUnits.mulRight · cited by 4AddUnits.mulRightisAddUnit_iff_exists · cited by 3isAddUnit_iff_existsAddUnits.neg_val · cited by 3AddUnits.neg_valAddLeftCancelMonoid.eq_zero_of_add_right · cited by 3AddLeftCancelMonoid.eq_ze…AddUnits.val_neg · cited by 3AddUnits.val_negAddRightCancelMonoid.eq_zero_of_add_right · cited by 2AddRightCancelMonoid.eq_z…AddUnits.neg_eq_val_neg · cited by 2AddUnits.neg_eq_val_negAddEquiv.val_neg_piAddUnits_apply · cited by 1AddEquiv.val_neg_piAddUni…eq_zero_of_add_left · cited by 1eq_zero_of_add_lefteq_zero_of_add_right · cited by 1eq_zero_of_add_rightAddUnits.val_neg_mulLeft · cited by 1AddUnits.val_neg_mulLeftAddUnits.val_neg_mulRight · cited by 1AddUnits.val_neg_mulRightAddMonoid · cited by 2864AddMonoidAddUnits · cited by 325AddUnitsAddUnits.negCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • AddMonoidstatement and proof · cited by 2,864
  • AddUnitsstatement and proof · cited by 325

Cited by18

Results whose statement or proof uses this declaration.