Regular elements #

Implementation details #

Group powers and other definitions import a lot of the algebra hierarchy. Lemmas about them are kept separate to be able to provide IsRegular early in the algebra hierarchy.

theorem IsLeftRegular.pow {R : Type u_1} {a : R} [] (n : ) (rla : ) :

Any power of a left-regular element is left-regular.

theorem IsRightRegular.pow {R : Type u_1} {a : R} [] (n : ) (rra : ) :

Any power of a right-regular element is right-regular.

theorem IsRegular.pow {R : Type u_1} {a : R} [] (n : ) (ra : ) :
IsRegular (a ^ n)

Any power of a regular element is regular.

theorem IsLeftRegular.pow_iff {R : Type u_1} {a : R} [] {n : } (n0 : 0 < n) :

An element a is left-regular if and only if a positive power of a is left-regular.

theorem IsRightRegular.pow_iff {R : Type u_1} {a : R} [] {n : } (n0 : 0 < n) :

An element a is right-regular if and only if a positive power of a is right-regular.

theorem IsRegular.pow_iff {R : Type u_1} {a : R} [] {n : } (n0 : 0 < n) :
IsRegular (a ^ n)

An element a is regular if and only if a positive power of a is regular.

theorem IsLeftRegular.prod {ι : Type u_2} {R : Type u_3} [] {s : } {f : ιR} (h : is, IsLeftRegular (f i)) :
IsLeftRegular (Finset.prod s fun (i : ι) => f i)
theorem IsRightRegular.prod {ι : Type u_2} {R : Type u_3} [] {s : } {f : ιR} (h : is, IsRightRegular (f i)) :
IsRightRegular (Finset.prod s fun (i : ι) => f i)
theorem IsRegular.prod {ι : Type u_2} {R : Type u_3} [] {s : } {f : ιR} (h : is, IsRegular (f i)) :
IsRegular (Finset.prod s fun (i : ι) => f i)