Results about IsRegular and pi types

@[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} : IsRegular a ↔ ∀ (i : ι), IsRegular (a 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