Results about IsRegular and ULift

@[simp]

theorem ULift.isLeftRegular_up {R : Type v} [Mul R] {a : R} : IsLeftRegular { down := a } ↔ IsLeftRegular a

@[simp]

theorem ULift.isAddLeftRegular_up {R : Type v} [Add R] {a : R} : IsAddLeftRegular { down := a } ↔ IsAddLeftRegular a

@[simp]

theorem ULift.isRightRegular_up {R : Type v} [Mul R] {a : R} : IsRightRegular { down := a } ↔ IsRightRegular a

@[simp]

theorem ULift.isAddRightRegular_up {R : Type v} [Add R] {a : R} : IsAddRightRegular { down := a } ↔ IsAddRightRegular a

@[simp]

theorem ULift.isRegular_up {R : Type v} [Mul R] {a : R} : IsRegular { down := a } ↔ IsRegular a

@[simp]

theorem ULift.isAddRegular_up {R : Type v} [Add R] {a : R} : IsAddRegular { down := a } ↔ IsAddRegular a

@[simp]

theorem ULift.isLeftRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} : IsLeftRegular a.down ↔ IsLeftRegular a

@[simp]

theorem ULift.isAddLeftRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} : IsAddLeftRegular a.down ↔ IsAddLeftRegular a

@[simp]

theorem ULift.isRightRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} : IsRightRegular a.down ↔ IsRightRegular a

@[simp]

theorem ULift.isAddRightRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} : IsAddRightRegular a.down ↔ IsAddRightRegular a

@[simp]

theorem ULift.isRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} : IsRegular a.down ↔ IsRegular a

@[simp]

theorem ULift.isAddRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} : IsAddRegular a.down ↔ IsAddRegular a

@[simp]

theorem ULift.isSMulRegular_iff {α : Type u_1} {R : Type v} [SMul α R] {r : α} : IsSMulRegular (ULift.{u_2, v} R) r ↔ IsSMulRegular R r