Documentation

Mathlib.Algebra.GroupWithZero.Regular

Results about IsRegular and 0 #

The element 0 is left-regular if and only if R is trivial.

The element 0 is right-regular if and only if R is trivial.

The element 0 is regular if and only if R is trivial.

The element 0 is left-regular if and only if R is trivial.

In a non-trivial MulZeroClass, the 0 element is not left-regular.

The element 0 is right-regular if and only if R is trivial.

In a non-trivial MulZeroClass, the 0 element is not right-regular.

The element 0 is regular if and only if R is trivial.

theorem IsLeftRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (la : IsLeftRegular a) :
a 0

A left-regular element of a Nontrivial MulZeroClass is non-zero.

theorem IsRightRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (ra : IsRightRegular a) :
a 0

A right-regular element of a Nontrivial MulZeroClass is non-zero.

theorem IsRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (la : IsRegular a) :
a 0

A regular element of a Nontrivial MulZeroClass is non-zero.

In a non-trivial ring, the element 0 is not left-regular -- with typeclasses.

In a non-trivial ring, the element 0 is not right-regular -- with typeclasses.

In a non-trivial ring, the element 0 is not regular -- with typeclasses.

@[simp]
theorem IsLeftRegular.mul_left_eq_zero_iff {R : Type u_1} [MulZeroClass R] {a b : R} (hb : IsLeftRegular b) :
b * a = 0 a = 0
@[simp]
theorem IsRightRegular.mul_right_eq_zero_iff {R : Type u_1} [MulZeroClass R] {a b : R} (hb : IsRightRegular b) :
a * b = 0 a = 0
theorem isRegular_of_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} (a0 : a 0) :

Non-zero elements of an integral domain are regular.

theorem isRegular_iff_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} [Nontrivial R] :

In a non-trivial integral domain, an element is regular iff it is non-zero.