Documentation

Mathlib.Algebra.GroupWithZero.Regular

Results about IsRegular and 0 #

source
theorem IsLeftRegular.subsingleton {R : Type u_1} [MulZeroClass R] (h : IsLeftRegular 0) :
Subsingleton R

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

source
theorem IsRightRegular.subsingleton {R : Type u_1} [MulZeroClass R] (h : IsRightRegular 0) :
Subsingleton R

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

source
theorem IsRegular.subsingleton {R : Type u_1} [MulZeroClass R] (h : IsRegular 0) :
Subsingleton R

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

source
theorem isLeftRegular_zero_iff_subsingleton {R : Type u_1} [MulZeroClass R] :
IsLeftRegular 0 ↔ Subsingleton R

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

source
theorem not_isLeftRegular_zero_iff {R : Type u_1} [MulZeroClass R] :
¬IsLeftRegular 0 ↔ Nontrivial R

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

source
theorem isRightRegular_zero_iff_subsingleton {R : Type u_1} [MulZeroClass R] :
IsRightRegular 0 ↔ Subsingleton R

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

source
theorem not_isRightRegular_zero_iff {R : Type u_1} [MulZeroClass R] :
¬IsRightRegular 0 ↔ Nontrivial R

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

source
theorem isRegular_iff_subsingleton {R : Type u_1} [MulZeroClass R] :
IsRegular 0 ↔ Subsingleton R

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

source
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.

source
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.

source
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.

source
theorem not_isLeftRegular_zero {R : Type u_1} [MulZeroClass R] [nR : Nontrivial R] :
¬IsLeftRegular 0

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

source
theorem not_isRightRegular_zero {R : Type u_1} [MulZeroClass R] [nR : Nontrivial R] :
¬IsRightRegular 0

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

source
theorem not_isRegular_zero {R : Type u_1} [MulZeroClass R] [Nontrivial R] :
¬IsRegular 0

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

source
@[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
source
@[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
source
theorem isRegular_of_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} (a0 : a ≠ 0) :
IsRegular a

Non-zero elements of an integral domain are regular.

source
theorem isRegular_iff_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} [Nontrivial R] :
IsRegular a ↔ a ≠ 0

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