Theorems · Theorem · ring theory
neg_mul_eq_neg_mul
∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = -a * b- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 20 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.
- neg_mulproof · cited by 654
- HasDistribNegstatement and proof · cited by 114
Cited by20
Results whose statement or proof uses this declaration.
- Complex.cosh_mul_Iproof · cited by 11
- Complex.sinh_mul_Iproof · cited by 10
- Complex.hasStrictDerivAt_cosproof · cited by 5
- mul_sub_right_distribproof · cited by 4
- Real.log_zpowproof · cited by 4
- EuclideanGeometry.dist_smul_vadd_eq_distproof · cited by 4
- intervalIntegral.integral_comp_sub_mulproof · cited by 3
- Zsqrtd.norm_nonnegproof · cited by 3
- Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_posproof · cited by 3
- Polynomial.mirror_negproof · cited by 2
- ZNum.mul_to_intproof · cited by 2
- MvPolynomial.mul_esymm_eq_sumproof · cited by 1