Regular elements #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
is_left_regular (a ^ n)
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) :
is_right_regular (a ^ n)
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) :
is_regular (a ^ n)
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) :
is_left_regular (a ^ n) ↔ is_left_regular a
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) :
is_right_regular (a ^ n) ↔ is_right_regular a
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) :
is_regular (a ^ n) ↔ is_regular a
An element a is regular if and only if a positive power of a is regular.