Theorems · Theorem · group theory
inv_ne_zero
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ ≠ 0- Defined in
- Mathlib.Algebra.GroupWithZero.NeZero
- Cited by
- 99 results in Mathlib
- Foundations
- Depth 12 from the axioms, rests on 112 definitions · uses propext
- Assumes
- GroupWithZero
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.
- MulZeroClass.mul_zeroproof · cited by 2,091
- GroupWithZerostatement and proof · cited by 691
- mul_inv_cancel₀proof · cited by 210
Cited by99
Results whose statement or proof uses this declaration.
- inv_mul_cancel₀proof · cited by 267
- Real.log_invproof · cited by 35
- zpow_ne_zeroproof · cited by 30
- div_ne_zeroproof · cited by 29
- RatFunc.num_div_denomproof · cited by 18
- MeasureTheory.Measure.addHaar_smulproof · cited by 13
- Polynomial.degree_mul_leadingCoeff_invproof · cited by 8
- Height.one_le_mulHeightproof · cited by 8
- Height.mulHeight_eq_one_of_subsingletonproof · cited by 7
- one_div_ne_zeroproof · cited by 7
- gauge_smul_of_nonnegproof · cited by 7
- IntervalIntegrable.comp_mul_leftproof · cited by 6