Theorems · Theorem · group theory
IsUnit.mk0
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (x : G₀), x ≠ 0 → IsUnit x- Cited by
- 33 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitstatement · cited by 1,602
- GroupWithZerostatement and proof · cited by 691
- Units.mk0proof · cited by 181
- Units.isUnitproof · cited by 116
Cited by33
Results whose statement or proof uses this declaration.
- Polynomial.irreducible_mul_leadingCoeff_invproof · cited by 6
- Polynomial.separable_X_pow_sub_Cproof · cited by 6
- MeasureTheory.integrable_smul_iffproof · cited by 5
- Polynomial.span_singleton_annIdealGeneratorproof · cited by 4
- eq_on_inv₀proof · cited by 3
- Algebra.discr_isUnit_of_basisproof · cited by 2
- Valuation.map_eq_one_of_forall_ltproof · cited by 2
- IsFractionRing.isUnit_map_of_injectiveproof · cited by 2
- IsIntegralClosure.isFractionRing_of_algebraicproof · cited by 2
- exists_pow_lt₀proof · cited by 2
- LinearMap.isBigOTVS_rev_compproof · cited by 2
- IsLocalization.isDedekindDomainproof · cited by 1