| Name | Category | Theorems |
|---|
IsAddLeftRegular 📖 | MathDef | 34 mathmath: IsDedekindFiniteAddMonoid.iff_isAddLeftRegular_of_add_eq_zero, IsAddLeftRegular.unop, ULift.isAddLeftRegular_up, isAddLeftRegular_ofDual, isAddRightRegular_op, isAddLeftRegular_ofColex, isLeftRegular_toMul, isLeftCancelAdd_iff, AddCommute.isAddRegular_iff, isAddLeftRegular_toLex, AddCommute.isAddRightRegular_iff, isAddRightRegular_unop, LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top, isAddLeftRegular_of_add_eq_zero, isAddLeftRegular_toAdd, isAddLeftRegular_unop, IsAddLeftRegular.all, isAddLeftRegular_op, isAddLeftRegular_toDual, isLeftRegular_ofAdd, IsLeftCancelAdd.add_left_cancel, IsAddLeftRegular.op, IsAddRightRegular.left_of_addCommute, isAddLeftRegular_iff_isAddRegular, isAddLeftRegular_ofMul, ULift.isAddLeftRegular_down, IsAddLeftRegular.nsmul_iff, isAddLeftRegular_ofLex, isAddLeftRegular_toColex, isAddRegular_iff, IsAddRegular.left, Pi.isAddLeftRegular_iff, Prod.isAddLeftRegular_mk, AddLECancellable.isAddLeftRegular
|
IsAddRegular 📖 | CompData | 31 mathmath: Pi.isAddRegular_iff, ArchimedeanClass.isAddRegular_mk, IsAddUnit.isAddRegular, AddSubmonoid.LocalizationMap.injective_iff, isCancelAdd_iff_forall_isAddRegular, isAddRegular_toAdd, isAddRegular_ofColex, isRegular_ofAdd, AddCommute.isAddRegular_iff, IsAddRegular.all, isAddRightRegular_iff_isAddRegular, isAddRegular_toLex, isAddRegular_zero, isAddRegular_add_and_add_iff, IsAddRegular.nsmul_iff, IsAddRegular.of_ne_top, isAddRegular_unop, AddUnits.isAddRegular, isAddRegular_ofMul, isAddRegular_ofDual, Prod.isAddRegular_mk, isAddLeftRegular_iff_isAddRegular, ULift.isAddRegular_down, isAddRegular_ofLex, isAddRegular_toColex, isRegular_toMul, isAddRegular_add_iff, isAddRegular_iff, isAddRegular_toDual, ULift.isAddRegular_up, isAddRegular_op
|
IsAddRightRegular 📖 | MathDef | 31 mathmath: isAddRightRegular_ofMul, isAddRightRegular_toColex, isAddRightRegular_op, isAddRightRegular_ofDual, Pi.isAddRightRegular_iff, ULift.isAddRightRegular_up, isAddRightRegular_toLex, isAddRightRegular_iff_isAddRegular, AddCommute.isAddRightRegular_iff, isAddRightRegular_unop, IsDedekindFiniteAddMonoid.iff_isAddRightRegular_of_add_eq_zero, IsAddRegular.right, isRightRegular_toMul, isAddRightRegular_toDual, isAddLeftRegular_unop, IsAddRightRegular.all, isAddRightRegular_ofLex, isAddLeftRegular_op, IsAddLeftRegular.right_of_addCommute, isAddRightRegular_ofColex, ULift.isAddRightRegular_down, IsAddRightRegular.op, IsAddRightRegular.unop, IsRightCancelAdd.add_right_cancel, isAddRightRegular_of_add_eq_zero, isAddRegular_iff, isRightCancelAdd_iff, isRightRegular_ofAdd, isAddRightRegular_toAdd, IsAddRightRegular.nsmul_iff, Prod.isAddRightRegular_mk
|
IsLeftRegular 📖 | MathDef | 49 mathmath: isLeftRegular_ofColex, isLeftRegular_of_non_zero_divisor, ULift.isLeftRegular_up, isLeftRegular_toLex, isRightRegular_star_iff, IsLeftCancelMul.mul_left_cancel, MulLECancellable.isLeftRegular, isLeftRegular_zero_iff_subsingleton, isRegular_iff, ULift.isLeftRegular_down, isLeftRegular_toMul, Pi.isLeftRegular_iff, IsLeftRegular.unop, isLeftRegular_iff_isRegular, not_isLeftRegular_zero, IsLeftCancelMulZero.mul_left_cancel_of_ne_zero, IsLeftRegular.all, Commute.isRightRegular_iff, IsRightRegular.left_of_commute, le_nonZeroDivisorsLeft_iff_isLeftRegular, IsDedekindFiniteMonoid.iff_isLeftRegular_of_mul_eq_one, isLeftRegular_of_mul_eq_one, Prod.isLeftRegular_mk, isLeftRegular_iff_mem_nonZeroDivisorsLeft, isAddLeftRegular_toAdd, isLeftRegular_ofDual, IsArtinianRing.isUnit_iff_isLeftRegular, IsRightRegular.star, IsSMulRegular.isLeftRegular, isLeftRegular_op, isLeftRegular_star_iff, isLeftRegular_ofAdd, not_isLeftRegular_zero_iff, isRightRegular_op, IsLeftRegular.pow_iff, Commute.isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isAddLeftRegular_ofMul, isLeftRegular_toDual, IsRegular.left, isLeftRegular_ofLex, isLeftCancelMul_iff, isLeftCancelMulZero_iff, isLeftRegular_iff, isRightRegular_unop, IsLeftRegular.op, Matrix.isLeftRegular_iff_mulVec_injective, isLeftRegular_unop, isLeftRegular_toColex
|
IsRegular 📖 | CompData | 55 mathmath: isRegular_iff_subsingleton, LinearMap.IsReflective.regular, Submonoid.LocalizationMap.injective_iff, isRegular_iff_eq_zero_of_mul, IsRegular.of_ne_zero, IsRegular.all, isRegular_toLex, isCancelMul_iff_forall_isRegular, IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite, isRegular_iff, isAddRegular_toAdd, Polynomial.isRegular_X, le_nonZeroDivisors_iff_isRegular, isRegular_iff_ne_zero, isRegular_of_ne_zero, Matrix.isRegular_of_isLeftRegular_det, IsLocalizedModule.isRegular_of_smul_left_injective, isRegular_ofAdd, isLeftRegular_iff_isRegular, Polynomial.Monic.isRegular, MvPolynomial.isRegular_prod_X, isRegular_star_iff, Prod.isRegular_mk, isRegular_mul_iff, isRegular_op, isRegular_of_ne_zero', IsRegular.of_ne_zero', isRegular_mul_and_mul_iff, Pi.isRegular_iff, MvPolynomial.isRegular_X, isRegular_iff_isUnit_of_finite, MvPolynomial.isRegular_X_pow, Polynomial.isRegular_X_pow, isRegular_iff_ne_zero', isAddRegular_ofMul, isRegular_iff_mem_nonZeroDivisors, IsUnit.isRegular, isRightRegular_iff_isRegular, Commute.isRegular_iff, IsLocalization.injective_iff_isRegular, ULift.isRegular_down, isRegular_toDual, not_isRegular_zero, IsRegular.pow_iff, isRegular_toMul, ULift.isRegular_up, isRegular_unop, Units.isRegular, isRegular_ofDual, isRegular_toColex, isRegular_one, isRegular_ofLex, isCancelMulZero_iff_forall_isRegular, IsArtinianRing.isUnit_iff_isRegular, isRegular_ofColex
|
IsRightRegular 📖 | MathDef | 47 mathmath: isAddRightRegular_ofMul, isRightRegular_star_iff, IsRightRegular.all, ULift.isRightRegular_up, isRightRegular_iff_mem_nonZeroDivisorsRight, isRightRegular_ofLex, IsRightRegular.op, not_isRightRegular_zero, IsLeftRegular.star, isRegular_iff, IsRightRegular.pow_iff, IsRegular.right, isRightRegular_of_non_zero_divisor, isRightRegular_toColex, Commute.isRightRegular_iff, Matrix.isRightRegular_iff_vecMul_injective, IsRightCancelMul.mul_right_cancel, isRightRegular_toDual, not_isRightRegular_zero_iff, isRightCancelMulZero_iff, isRightRegular_toLex, isRightRegular_toMul, IsDedekindFiniteMonoid.iff_isRightRegular_of_mul_eq_one, Prod.isRightRegular_mk, isLeftRegular_op, isLeftRegular_star_iff, Pi.isRightRegular_iff, ULift.isRightRegular_down, isRightRegular_of_mul_eq_one, IsSMulRegular.isRightRegular, isRightRegular_iff, isRightRegular_ofDual, isRightRegular_op, isRightRegular_ofColex, isRightRegular_iff_isRegular, IsRightRegular.unop, IsRightCancelMulZero.mul_right_cancel_of_ne_zero, isRightRegular_zero_iff_subsingleton, isRightRegular_ofAdd, isAddRightRegular_toAdd, isRightRegular_iff_left_eq_zero_of_mul, IsArtinianRing.isUnit_iff_isRightRegular, isRightCancelMul_iff, isRightRegular_unop, le_nonZeroDivisorsRight_iff_isRightRegular, isLeftRegular_unop, IsLeftRegular.right_of_commute
|