Theorems · Theorem · group theory
IsUnit.ne_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] {a : M₀}, IsUnit a → a ≠ 0- Cited by
- 36 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- MonoidWithZeroNontrivial
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.
- Unitsproof · cited by 2,804
- Nontrivialstatement and proof · cited by 2,416
- Units.valproof · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- MonoidWithZerostatement and proof · cited by 456
- Units.ne_zeroproof · cited by 68
Cited by36
Results whose statement or proof uses this declaration.
- Polynomial.degree_eq_zero_of_isUnitproof · cited by 14
- Polynomial.IsPrimitive.ne_zeroproof · cited by 4
- WeierstrassCurve.Projective.Point.toAffine_smulproof · cited by 3
- MeasureTheory.Measure.addHaar_preimage_linearEquivproof · cited by 3
- CharP.isUnit_natCast_iffproof · cited by 3
- WeierstrassCurve.Jacobian.Point.toAffine_smulproof · cited by 3
- Char.card_pow_char_powproof · cited by 2
- ENNReal.isUnit_iffproof · cited by 2
- Module.Basis.orientation_eq_iff_det_posproof · cited by 2
- MeasureTheory.hausdorffMeasure_homothety_preimageproof · cited by 2
- IsFractionRing.nontrivial_iff_nontrivialproof · cited by 2
- LinearEquiv.det_coe_symmproof · cited by 2