Theorems · Theorem · ring theory
neg_mul_eq_mul_neg
∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = a * -b- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- MulHasDistribNeg
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_negproof · cited by 590
- HasDistribNegstatement and proof · cited by 114
Cited by15
Results whose statement or proof uses this declaration.
- mul_sub_left_distribproof · cited by 9
- div_neg_eq_neg_divproof · cited by 6
- AkraBazziRecurrence.GrowsPolynomially.negproof · cited by 4
- Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_negproof · cited by 3
- Filter.Tendsto.atTop_mul_negproof · cited by 3
- Zsqrtd.norm_eq_one_iffproof · cited by 3
- mul_nonpos_iffproof · cited by 2
- ZNum.mul_to_intproof · cited by 2
- mul_neg_iffproof · cited by 2
- map_le_lineMap_iff_slope_le_slope_rightproof · cited by 2
- Subring.InClosure.recOnproof · cited by 2
- DihedralGroup.r_zpowproof · cited by 1