Theorems · Theorem · group theory
Units.ne_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] (u : M₀ˣ), ↑u ≠ 0An element of the unit group of a nonzero monoid with zero represented as an element of the monoid is nonzero.
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 9 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.
- Unitsstatement and proof · cited by 2,804
- Nontrivialstatement and proof · cited by 2,416
- Units.valstatement · cited by 1,966
- MonoidWithZerostatement and proof · cited by 456
- Units.mul_invproof · cited by 67
- left_ne_zero_of_mul_eq_oneproof · cited by 6
Cited by68
Results whose statement or proof uses this declaration.
- IsUnit.ne_zeroproof · cited by 36
- Matrix.GeneralLinearGroup.det_ne_zeroproof · cited by 13
- NumberField.Units.coe_ne_zeroproof · cited by 5
- ClassGroup.mk0_surjectiveproof · cited by 5
- units_inv_smulproof · cited by 4
- UpperHalfPlane.denom_ne_zero_of_improof · cited by 4
- ClassGroup.mk_eq_one_iffproof · cited by 4
- ZLattice.volume_image_eq_volume_div_covolumeproof · cited by 3
- units_smul_eq_self_iffproof · cited by 3
- MonoidWithZeroHom.mem_valueGroup_iff_of_commproof · cited by 3
- Valuation.IsUniformizer.ne_zeroproof · cited by 3
- Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injectiveproof · cited by 2