Mathlib Map

Theorems · Theorem · ring theory

Units.val_neg

∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑u

Representing an element of a ring's unit group as an element of the ring commutes with mapping this element to its additive inverse.

Defined in
Mathlib.Algebra.Ring.Units
Cited by
6 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext
Assumes
MonoidHasDistribNeg
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Units.neg_smul · cited by 27Units.neg_smulFunction.Antiperiodic.add_zsmul_eq · cited by 3Antiperiodic.add_zsmul_eqNumberField.Units.even_torsionOrder · cited by 3Units.even_torsionOrderunits_smul_eq_neg_iff · cited by 2units_smul_eq_neg_iffInt.normalize_of_nonpos · cited by 2Int.normalize_of_nonposModule.Ray.units_smul_of_neg · cited by 0Ray.units_smul_of_negMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valHasDistribNeg · cited by 114HasDistribNegUnits.val_negCITED BYCITES

Cites4

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

  • Monoidstatement and proof · cited by 3,887
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement · cited by 1,966
  • HasDistribNegstatement and proof · cited by 114

Cited by6

Results whose statement or proof uses this declaration.