Mathlib Map

Theorems · Theorem · ring theory

Units.neg_divp

∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ u
Defined in
Mathlib.Algebra.Ring.Units
Cited by
2 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext
Assumes
MonoidHasDistribNeg
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Units.divp_sub_divp_same · cited by 0Units.divp_sub_divp_sameUnits.divp_sub_divp · cited by 0Units.divp_sub_divpMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valneg_mul · cited by 654neg_mulHasDistribNeg · cited by 114HasDistribNegdivp · cited by 34divpUnits.neg_divpCITED BYCITES

Cites6

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.valproof · cited by 1,966
  • neg_mulproof · cited by 654
  • HasDistribNegstatement and proof · cited by 114
  • divpstatement · cited by 34

Cited by2

Results whose statement or proof uses this declaration.