Theorems · Theorem · ring theory
neg_div_neg_eq
∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a b : R), -a / -b = a / b- Defined in
- Mathlib.Algebra.Ring.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- DivisionMonoidHasDistribNeg
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- neg_negproof · cited by 960
- DivisionMonoidstatement and proof · cited by 201
- neg_divproof · cited by 161
- HasDistribNegstatement and proof · cited by 114
- div_neg_eq_neg_divproof · cited by 6
Cited by17
Results whose statement or proof uses this declaration.
- jacobiTheta₂_functional_equationproof · cited by 3
- ConvexOn.secant_monoproof · cited by 3
- StrictConvexOn.secant_strict_monoproof · cited by 3
- UpperHalfPlane.neg_smulproof · cited by 3
- HasDerivAt.lhopital_zero_left_on_Iooproof · cited by 3
- geom_sum_Ico'proof · cited by 2
- Function.Antiperiodic.divproof · cited by 2
- Complex.tanh_periodicproof · cited by 2
- HasDerivAt.lhopital_zero_atBot_on_Iioproof · cited by 2
- IsCauSeq.geo_seriesproof · cited by 1
- div_le_one_of_geproof · cited by 1
- ProbabilityTheory.lintegral_paretoPDF_eq_oneproof · cited by 1