Theorems · Theorem · group theory
Invertible.ne_zero
∀ {α : Type u} [inst : MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a], a ≠ 0- Defined in
- Mathlib.Algebra.GroupWithZero.Invertible
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nontrivialstatement and proof · cited by 2,416
- MulZeroClass.mul_zeroproof · cited by 2,091
- Invertiblestatement and proof · cited by 549
- Invertible.invOfproof · cited by 268
- MulZeroOneClassstatement and proof · cited by 184
- zero_ne_oneproof · cited by 90
- Invertible.invOf_mul_selfproof · cited by 3
Cited by10
Results whose statement or proof uses this declaration.
- invOf_eq_invproof · cited by 42
- mul_inv_cancel_of_invertibleproof · cited by 4
- inv_mul_cancel_of_invertibleproof · cited by 2
- div_self_of_invertibleproof · cited by 1
- div_mul_cancel_of_invertibleproof · cited by 1
- pos_of_invertible_castproof · cited by 1
- xInTermsOfW_vars_auxproof · cited by 1
- Finset.centroid_pairproof · cited by 1
- mul_div_cancel_of_invertibleproof · cited by 0
- not_ringChar_dvd_of_invertibleproof · cited by 0