Theorems · Theorem · commutative algebra
one_sub_invOf_two
∀ {R : Type u_1} [inst : Ring R] [inst_1 : Invertible 2], 1 - ⅟2 = ⅟2- Defined in
- Mathlib.Algebra.Ring.Invertible
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- RingInvertible
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- mul_oneproof · cited by 3,885
- Invertiblestatement and proof · cited by 549
- Invertible.invOfstatement and proof · cited by 268
- mul_subproof · cited by 201
- add_sub_cancel_rightproof · cited by 187
- one_add_one_eq_twoproof · cited by 65
- mul_invOf_selfproof · cited by 28
- isUnit_of_invertibleproof · cited by 26
- IsUnit.mul_right_injproof · cited by 13
Cited by1
Results whose statement or proof uses this declaration.
- midpoint_commproof · cited by 14