@[simp]
theorem
Prod.isLeftRegular_mk
{R : Type u_2}
{S : Type u_3}
[Mul R]
[Mul S]
{a : R}
{b : S}
:
IsLeftRegular (a, b) ↔ IsLeftRegular a ∧ IsLeftRegular b
@[simp]
theorem
Prod.isAddLeftRegular_mk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
:
IsAddLeftRegular (a, b) ↔ IsAddLeftRegular a ∧ IsAddLeftRegular b
@[simp]
theorem
Prod.isRightRegular_mk
{R : Type u_2}
{S : Type u_3}
[Mul R]
[Mul S]
{a : R}
{b : S}
:
IsRightRegular (a, b) ↔ IsRightRegular a ∧ IsRightRegular b
@[simp]
theorem
Prod.isAddRightRegular_mk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
:
IsAddRightRegular (a, b) ↔ IsAddRightRegular a ∧ IsAddRightRegular b
@[simp]
@[simp]
theorem
Prod.isAddRegular_mk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
:
IsAddRegular (a, b) ↔ IsAddRegular a ∧ IsAddRegular b
theorem
IsLeftRegular.prodMk
{R : Type u_2}
{S : Type u_3}
[Mul R]
[Mul S]
{a : R}
{b : S}
(ha : IsLeftRegular a)
(hb : IsLeftRegular b)
:
IsLeftRegular (a, b)
theorem
IsAddLeftRegular.sumMk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
(ha : IsAddLeftRegular a)
(hb : IsAddLeftRegular b)
:
IsAddLeftRegular (a, b)
theorem
IsRightRegular.prodMk
{R : Type u_2}
{S : Type u_3}
[Mul R]
[Mul S]
{a : R}
{b : S}
(ha : IsRightRegular a)
(hb : IsRightRegular b)
:
IsRightRegular (a, b)
theorem
IsAddRightRegular.sumMk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
(ha : IsAddRightRegular a)
(hb : IsAddRightRegular b)
:
IsAddRightRegular (a, b)
theorem
IsAddRegular.sumMk
{R : Type u_2}
{S : Type u_3}
[Add R]
[Add S]
{a : R}
{b : S}
(ha : IsAddRegular a)
(hb : IsAddRegular b)
:
IsAddRegular (a, b)
@[simp]
theorem
Prod.isSMulRegular_iff
{α : Type u_1}
{R : Type u_2}
{S : Type u_3}
[SMul α R]
[SMul α S]
{r : α}
[Nonempty R]
[Nonempty S]
:
IsSMulRegular (R × S) r ↔ IsSMulRegular R r ∧ IsSMulRegular S r