mathlib documentation

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 is_regular early in the algebra hierarchy.

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

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

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

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

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

Any power of a regular element is regular.

theorem is_left_regular.pow_iff {R : Type u_1} {a : R} [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 is_right_regular.pow_iff {R : Type u_1} {a : R} [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 is_regular.pow_iff {R : Type u_1} {a : R} [monoid R] {n : } (n0 : 0 < n) :

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