Theorems · Theorem · commutative algebra
invOf_neg
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) [inst_2 : Invertible a]
[inst_3 : Invertible (-a)], ⅟(-a) = -⅟a- Defined in
- Mathlib.Algebra.Ring.Invertible
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- neg_negproof · cited by 960
- neg_mulproof · cited by 654
- mul_negproof · cited by 590
- Invertiblestatement and proof · cited by 549
- Invertible.invOfstatement and proof · cited by 268
- HasDistribNegstatement and proof · cited by 114
- mul_invOf_self'proof · cited by 16
- invOf_eq_right_invproof · cited by 10
Cited by2
Results whose statement or proof uses this declaration.
- lipschitzGroup.involute_act_ι_mem_range_ιproof · cited by 2
- Polynomial.dvd_comp_neg_X_iffproof · cited by 0