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}
[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}
[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}
[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}
[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.
theorem
IsLeftRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsLeftRegular (f i))
:
IsLeftRegular (∏ i ∈ s, f i)
theorem
IsRightRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsRightRegular (f i))
:
IsRightRegular (∏ i ∈ s, f i)
theorem
IsRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsRegular (f i))
:
IsRegular (∏ i ∈ s, f i)