Mathlib.Algebra.Regular.Pow

Module docstring

{"# Product of regular elements

TODO

Move to Mathlib.Algebra.BigOperators.Group.Finset.Basic? "}

IsLeftRegular.prod theorem

(h : ∀ i ∈ s, IsLeftRegular (f i)) : IsLeftRegular (∏ i ∈ s, f i)

Full source

lemma IsLeftRegular.prod (h : ∀ i ∈ s, IsLeftRegular (f i)) :
    IsLeftRegular (∏ i ∈ s, f i) :=
  s.prod_induction _ _ (@IsLeftRegular.mul R _) isRegular_one.left h

Product of Left Regular Elements is Left Regular

Informal description

Let $M$ be a commutative monoid, $s$ a finite set, and $f : \alpha \to M$ a function. If for every $i \in s$, the element $f(i)$ is left regular (i.e., left multiplication by $f(i)$ is injective), then the product $\prod_{i \in s} f(i)$ is also left regular.

IsRightRegular.prod theorem

(h : ∀ i ∈ s, IsRightRegular (f i)) : IsRightRegular (∏ i ∈ s, f i)

Full source

lemma IsRightRegular.prod (h : ∀ i ∈ s, IsRightRegular (f i)) :
    IsRightRegular (∏ i ∈ s, f i) :=
  s.prod_induction _ _ (@IsRightRegular.mul R _) isRegular_one.right h

Product of Right Regular Elements is Right Regular

Informal description

Let $M$ be a commutative monoid, $s$ a finite set, and $f : \alpha \to M$ a function. If for every $i \in s$, the element $f(i)$ is right regular (i.e., $f(i) \cdot a = f(i) \cdot b$ implies $a = b$ for all $a, b \in M$), then the product $\prod_{i \in s} f(i)$ is also right regular.

IsRegular.prod theorem

(h : ∀ i ∈ s, IsRegular (f i)) : IsRegular (∏ i ∈ s, f i)

Full source

lemma IsRegular.prod (h : ∀ i ∈ s, IsRegular (f i)) :
    IsRegular (∏ i ∈ s, f i) :=
  ⟨IsLeftRegular.prod fun a ha ↦ (h a ha).left,
   IsRightRegular.prod fun a ha ↦ (h a ha).right⟩

Product of Regular Elements is Regular

Informal description

Let $M$ be a commutative monoid, $s$ a finite set, and $f : \alpha \to M$ a function. If for every $i \in s$, the element $f(i)$ is regular (i.e., both left and right multiplication by $f(i)$ are injective), then the product $\prod_{i \in s} f(i)$ is also regular.