Documentation

Mathlib.Algebra.Regular.Prod

Results about IsRegular and Prod #

source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem Prod.isRegular_mk {R : Type u_2} {S : Type u_3} [Mul R] [Mul S] {a : R} {b : S} :
IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b
source
@[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
source
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)
source
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)
source
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)
source
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)
source
theorem IsRegular.prodMk {R : Type u_2} {S : Type u_3} [Mul R] [Mul S] {a : R} {b : S} (ha : IsRegular a) (hb : IsRegular b) :
IsRegular (a, b)
source
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)
source
@[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