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} [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} [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} [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} [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} [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} [Monoid R] {n : } (n0 : 0 < n) :

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

theorem IsLeftRegular.prod {ι : Type u_2} {R : Type u_3} [CommMonoid R] {s : Finset ι} {f : ιR} (h : ∀ (i : ι), i sIsLeftRegular (f i)) :
IsLeftRegular (Finset.prod s fun i => f i)
theorem IsRightRegular.prod {ι : Type u_2} {R : Type u_3} [CommMonoid R] {s : Finset ι} {f : ιR} (h : ∀ (i : ι), i sIsRightRegular (f i)) :
IsRightRegular (Finset.prod s fun i => f i)
theorem IsRegular.prod {ι : Type u_2} {R : Type u_3} [CommMonoid R] {s : Finset ι} {f : ιR} (h : ∀ (i : ι), i sIsRegular (f i)) :
IsRegular (Finset.prod s fun i => f i)