Theorems · Theorem · ring theory
inv_neg
∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] {a : R}, (-a)⁻¹ = -a⁻¹- Defined in
- Mathlib.Algebra.Ring.Basic
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- DivisionMonoidHasDistribNeg
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DivisionMonoidstatement and proof · cited by 201
- HasDistribNegstatement and proof · cited by 114
- neg_invproof · cited by 11
Cited by42
Results whose statement or proof uses this declaration.
- Int.negOnePow_negproof · cited by 13
- inv_lt_zero'proof · cited by 11
- UpperHalfPlane.modular_S_smulproof · cited by 9
- UpperHalfPlane.im_inv_neg_coe_posproof · cited by 7
- intervalIntegral.integral_comp_sub_mulproof · cited by 3
- Hyperreal.infiniteNeg_iff_infinitesimal_inv_negproof · cited by 3
- map_inv_intCast_smulproof · cited by 3
- Affine.Simplex.exsphere_complproof · cited by 3
- interval_average_eqproof · cited by 3
- Real.deriv_inv_log_applyproof · cited by 2
- Real.deriv_log_log_applyproof · cited by 2
- Affine.Simplex.excenterWeights_complproof · cited by 2