Theorems · Theorem · group theory
invOf_eq_inv
∀ {α : Type u} [inst : GroupWithZero α] (a : α) [inst_1 : Invertible a], ⅟a = a⁻¹- Defined in
- Mathlib.Algebra.GroupWithZero.Invertible
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZeroInvertible
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GroupWithZerostatement and proof · cited by 691
- Invertiblestatement and proof · cited by 549
- Invertible.invOfstatement · cited by 268
- mul_inv_cancel₀proof · cited by 210
- invOf_eq_right_invproof · cited by 10
- Invertible.ne_zeroproof · cited by 10
Cited by42
Results whose statement or proof uses this declaration.
- realPart_add_I_smul_imaginaryPartproof · cited by 10
- realPart_apply_coeproof · cited by 9
- dist_left_midpointproof · cited by 7
- imaginaryPart_apply_coeproof · cited by 6
- Urysohns.CU.approx_le_oneproof · cited by 4
- dist_midpoint_midpoint_le'proof · cited by 2
- EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radiusproof · cited by 2
- EuclideanGeometry.angle_midpoint_eq_piproof · cited by 1
- TrivSqZeroExt.invOf_eq_invproof · cited by 1
- Mathlib.Meta.Positivity.log_pos_of_isNNRatproof · cited by 1
- Polynomial.Chebyshev.C_two_mul_complex_cosproof · cited by 1