Documentation

Mathlib.Algebra.Regular.ULift

Results about IsRegular and ULift #

source
@[simp]
theorem ULift.isLeftRegular_up {R : Type v} [Mul R] {a : R} :
IsLeftRegular { down := a } ↔ IsLeftRegular a
source
@[simp]
theorem ULift.isAddLeftRegular_up {R : Type v} [Add R] {a : R} :
IsAddLeftRegular { down := a } ↔ IsAddLeftRegular a
source
@[simp]
theorem ULift.isRightRegular_up {R : Type v} [Mul R] {a : R} :
IsRightRegular { down := a } ↔ IsRightRegular a
source
@[simp]
theorem ULift.isAddRightRegular_up {R : Type v} [Add R] {a : R} :
IsAddRightRegular { down := a } ↔ IsAddRightRegular a
source
@[simp]
theorem ULift.isRegular_up {R : Type v} [Mul R] {a : R} :
IsRegular { down := a } ↔ IsRegular a
source
@[simp]
theorem ULift.isAddRegular_up {R : Type v} [Add R] {a : R} :
IsAddRegular { down := a } ↔ IsAddRegular a
source
@[simp]
theorem ULift.isLeftRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} :
IsLeftRegular a.down ↔ IsLeftRegular a
source
@[simp]
theorem ULift.isAddLeftRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} :
IsAddLeftRegular a.down ↔ IsAddLeftRegular a
source
@[simp]
theorem ULift.isRightRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} :
IsRightRegular a.down ↔ IsRightRegular a
source
@[simp]
theorem ULift.isAddRightRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} :
IsAddRightRegular a.down ↔ IsAddRightRegular a
source
@[simp]
theorem ULift.isRegular_down {R : Type v} [Mul R] {a : ULift.{u, v} R} :
IsRegular a.down ↔ IsRegular a
source
@[simp]
theorem ULift.isAddRegular_down {R : Type v} [Add R] {a : ULift.{u, v} R} :
IsAddRegular a.down ↔ IsAddRegular a
source
@[simp]
theorem ULift.isSMulRegular_iff {α : Type u_1} {R : Type v} [SMul α R] {r : α} :
IsSMulRegular (ULift.{u_2, v} R) r ↔ IsSMulRegular R r