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)
:
IsLeftRegular (a ^ n)
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)
:
IsRightRegular (a ^ n)
Any power of a right-regular element is right-regular.
theorem
IsLeftRegular.pow_iff
{R : Type u_1}
{a : R}
[inst : Monoid R]
{n : ℕ}
(n0 : 0 < n)
:
IsLeftRegular (a ^ n) ↔ IsLeftRegular a
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)
:
IsRightRegular (a ^ n) ↔ IsRightRegular a
An element a is right-regular if and only if a positive power of a is right-regular.