@[simp]
theorem
Pi.isLeftRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Mul (R i)]
{a : (i : ι) → R i}
:
IsLeftRegular a ↔ ∀ (i : ι), IsLeftRegular (a i)
@[simp]
theorem
Pi.isAddLeftRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Add (R i)]
{a : (i : ι) → R i}
:
IsAddLeftRegular a ↔ ∀ (i : ι), IsAddLeftRegular (a i)
@[simp]
theorem
Pi.isRightRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Mul (R i)]
{a : (i : ι) → R i}
:
IsRightRegular a ↔ ∀ (i : ι), IsRightRegular (a i)
@[simp]
theorem
Pi.isAddRightRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Add (R i)]
{a : (i : ι) → R i}
:
IsAddRightRegular a ↔ ∀ (i : ι), IsAddRightRegular (a i)
@[simp]
theorem
Pi.isRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Mul (R i)]
{a : (i : ι) → R i}
:
@[simp]
theorem
Pi.isAddRegular_iff
{ι : Type u_1}
{R : ι → Type u_3}
[(i : ι) → Add (R i)]
{a : (i : ι) → R i}
:
IsAddRegular a ↔ ∀ (i : ι), IsAddRegular (a i)
@[simp]
theorem
Pi.isSMulRegular_iff
{ι : Type u_1}
{α : Type u_2}
{R : ι → Type u_3}
[(i : ι) → SMul α (R i)]
{r : α}
[∀ (i : ι), Nonempty (R i)]
:
IsSMulRegular ((i : ι) → R i) r ↔ ∀ (i : ι), IsSMulRegular (R i) r