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 : Monoid R] (n : ) (rla : IsLeftRegular a) :

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

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

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

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

Any power of a regular element is regular.

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

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