Documentation

Mathlib.Algebra.Regular.Opposite

Results about IsRegular and MulOpposite #

source
๐Ÿ“ coverage
@[simp]
theorem isLeftRegular_op {R : Type u_1} [Mul R] {a : R} :
IsLeftRegular (MulOpposite.op a) โ†” IsRightRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddLeftRegular_op {R : Type u_1} [Add R] {a : R} :
IsAddLeftRegular (AddOpposite.op a) โ†” IsAddRightRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isRightRegular_op {R : Type u_1} [Mul R] {a : R} :
IsRightRegular (MulOpposite.op a) โ†” IsLeftRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddRightRegular_op {R : Type u_1} [Add R] {a : R} :
IsAddRightRegular (AddOpposite.op a) โ†” IsAddLeftRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isRegular_op {R : Type u_1} [Mul R] {a : R} :
IsRegular (MulOpposite.op a) โ†” IsRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddRegular_op {R : Type u_1} [Add R] {a : R} :
IsAddRegular (AddOpposite.op a) โ†” IsAddRegular a
source
๐Ÿ“ coverage
theorem IsLeftRegular.op {R : Type u_1} [Mul R] {a : R} :
IsRightRegular a โ†’ IsLeftRegular (MulOpposite.op a)

Alias of the reverse direction of isLeftRegular_op.

source
๐Ÿ“ coverage
theorem IsAddLeftRegular.op {R : Type u_1} [Add R] {a : R} :
IsAddRightRegular a โ†’ IsAddLeftRegular (AddOpposite.op a)
source
๐Ÿ“ coverage
theorem IsRightRegular.op {R : Type u_1} [Mul R] {a : R} :
IsLeftRegular a โ†’ IsRightRegular (MulOpposite.op a)

Alias of the reverse direction of isRightRegular_op.

source
๐Ÿ“ coverage
theorem IsAddRightRegular.op {R : Type u_1} [Add R] {a : R} :
IsAddLeftRegular a โ†’ IsAddRightRegular (AddOpposite.op a)
source
๐Ÿ“ coverage
theorem IsRegular.op {R : Type u_1} [Mul R] {a : R} :
IsRegular a โ†’ IsRegular (MulOpposite.op a)

Alias of the reverse direction of isRegular_op.

source
๐Ÿ“ coverage
theorem IsAddRegular.op {R : Type u_1} [Add R] {a : R} :
IsAddRegular a โ†’ IsAddRegular (AddOpposite.op a)
source
๐Ÿ“ coverage
@[simp]
theorem isLeftRegular_unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsLeftRegular (MulOpposite.unop a) โ†” IsRightRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddLeftRegular_unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddLeftRegular (AddOpposite.unop a) โ†” IsAddRightRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isRightRegular_unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsRightRegular (MulOpposite.unop a) โ†” IsLeftRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddRightRegular_unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddRightRegular (AddOpposite.unop a) โ†” IsAddLeftRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isRegular_unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsRegular (MulOpposite.unop a) โ†” IsRegular a
source
๐Ÿ“ coverage
@[simp]
theorem isAddRegular_unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddRegular (AddOpposite.unop a) โ†” IsAddRegular a
source
๐Ÿ“ coverage
theorem IsLeftRegular.unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsRightRegular a โ†’ IsLeftRegular (MulOpposite.unop a)

Alias of the reverse direction of isLeftRegular_unop.

source
๐Ÿ“ coverage
theorem IsAddLeftRegular.unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddRightRegular a โ†’ IsAddLeftRegular (AddOpposite.unop a)
source
๐Ÿ“ coverage
theorem IsRightRegular.unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsLeftRegular a โ†’ IsRightRegular (MulOpposite.unop a)

Alias of the reverse direction of isRightRegular_unop.

source
๐Ÿ“ coverage
theorem IsAddRightRegular.unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddLeftRegular a โ†’ IsAddRightRegular (AddOpposite.unop a)
source
๐Ÿ“ coverage
theorem IsRegular.unop {R : Type u_1} [Mul R] {a : Rแตแต’แต–} :
IsRegular a โ†’ IsRegular (MulOpposite.unop a)

Alias of the reverse direction of isRegular_unop.

source
๐Ÿ“ coverage
theorem IsAddRegular.unop {R : Type u_1} [Add R] {a : Rแตƒแต’แต–} :
IsAddRegular a โ†’ IsAddRegular (AddOpposite.unop a)