Theorems · Theorem · group theory
IsRegular.ne_zero
∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [Nontrivial R], IsRegular a → a ≠ 0A regular element of a Nontrivial MulZeroClass is non-zero.
- Defined in
- Mathlib.Algebra.GroupWithZero.Regular
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses propext
- Assumes
- MulZeroClassNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- MulZeroClassstatement and proof · cited by 232
- IsRegularstatement and proof · cited by 116
- IsRegular.leftproof · cited by 39
- IsLeftRegular.ne_zeroproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- Module.IsTorsionFree.trans_faithfulSMulproof · cited by 6
- Module.IsTorsionFree.of_smul_eq_zeroproof · cited by 2
- star_mul_self_posproof · cited by 2
- MonomialOrder.degree_prod_of_regularproof · cited by 1
- HahnSeries.order_single_mul_of_isRegularproof · cited by 1
- isRegular_iff_ne_zeroproof · cited by 0
- not_isRegular_zeroproof · cited by 0