# Documentation

Mathlib.Algebra.Regular.Pow

# 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} [inst : ] (n : ) (rla : ) :

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

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

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

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

Any power of a regular element is regular.

theorem IsLeftRegular.pow_iff {R : Type u_1} {a : R} [inst : ] {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} [inst : ] {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} [inst : ] {n : } (n0 : 0 < n) :
IsRegular (a ^ n)

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