SMul

📁 Source: Mathlib/Algebra/Regular/SMul.lean

Statistics

Metric	Count
Definitions	0
Theorems `isSMulRegular_congr`, `isSMulRegular`, `isSMulRegular`, `isLeftRegular`, `isRightRegular`, `map`, `mul`, `mul_and_mul_iff`, `mul_iff`, `mul_iff_right`, `natAbs_iff`, `not_zero`, `not_zero_iff`, `of_map`, `of_mul`, `of_mul_eq_one`, `of_right_eq_zero_of_smul`, `of_smul`, `of_smul_eq_one`, `one`, `pow`, `pow_iff`, `right_eq_zero_of_smul`, `smul`, `smul_iff`, `subsingleton`, `zero`, `zero_iff_subsingleton`, `isSMulRegular`, `isSMulRegular`, `isLeftRegular_iff`, `isRightRegular_iff`, `isSMulRegular_iff_right_eq_zero_of_smul`, `isSMulRegular_map`, `isSMulRegular_of_group`	35
Total	35

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSMulRegular_congr` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	`IsSMulRegular`	—	`comp_injective` `injective_comp`

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSMulRegular` 📖	mathematical	`IsLeftRegular`	`IsSMulRegular`	—	—

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSMulRegular` 📖	mathematical	`IsRightRegular`	`IsSMulRegular` `MulOpposite` `Mul.toSMulMulOpposite` `MulOpposite.op`	—	—

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftRegular` 📖	mathematical	`IsSMulRegular`	`IsLeftRegular`	—	—
`isRightRegular` 📖	mathematical	`IsSMulRegular` `MulOpposite` `Mul.toSMulMulOpposite` `MulOpposite.op`	`IsRightRegular`	—	—
`map` 📖	—	`IsSMulRegular`	—	—	`isSMulRegular_map`
`mul` 📖	—	`IsSMulRegular`	—	—	`smul`
`mul_and_mul_iff` 📖	mathematical	—	`IsSMulRegular`	—	`of_mul` `mul`
`mul_iff` 📖	mathematical	—	`IsSMulRegular` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`mul_and_mul_iff` `mul_comm`
`mul_iff_right` 📖	—	`IsSMulRegular`	—	—	`of_mul` `mul`
`natAbs_iff` 📖	mathematical	—	`IsSMulRegular` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubNegMonoid.toZSMul`	—	`natCast_zsmul` `zero_nsmul` `zero_zsmul` `neg_zsmul`
`not_zero` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero`	—	`not_zero_iff`
`not_zero_iff` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero` `Nontrivial`	—	`nontrivial_iff` `not_iff_comm` `zero_iff_subsingleton` `subsingleton_iff`
`of_map` 📖	—	`IsSMulRegular`	—	—	`isSMulRegular_map`
`of_mul` 📖	—	`IsSMulRegular`	—	—	`of_smul` `smul_eq_mul`
`of_mul_eq_one` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`of_mul` `IsScalarTower.left` `one`
`of_right_eq_zero_of_smul` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass`	—	`isSMulRegular_iff_right_eq_zero_of_smul`
`of_smul` 📖	—	`IsSMulRegular`	—	—	`Function.Injective.of_comp` `smul_assoc`
`of_smul_eq_one` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`of_smul` `one`
`one` 📖	mathematical	—	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_smul`
`pow` 📖	mathematical	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`Monoid.toNatPow`	—	`pow_zero` `pow_succ'` `smul_iff` `IsScalarTower.left`
`pow_iff` 📖	mathematical	—	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toNatPow`	—	`pow_succ` `smul_eq_mul` `of_smul` `IsScalarTower.left` `pow`
`right_eq_zero_of_smul` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul`	—	—	`smul_zero`
`smul` 📖	—	`IsSMulRegular`	—	—	`smul_assoc`
`smul_iff` 📖	—	`IsSMulRegular`	—	—	`of_smul` `smul`
`subsingleton` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero`	—	—	`MulActionWithZero.zero_smul`
`zero` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero`	—	`zero_iff_subsingleton`
`zero_iff_subsingleton` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero`	—	`subsingleton`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSMulRegular` 📖	mathematical	`IsUnit`	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Units.isSMulRegular`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSMulRegular` 📖	mathematical	—	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `val`	—	`IsSMulRegular.of_mul_eq_one` `inv_val`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftRegular_iff` 📖	mathematical	—	`IsLeftRegular` `IsSMulRegular`	—	—
`isRightRegular_iff` 📖	mathematical	—	`IsRightRegular` `IsSMulRegular` `MulOpposite` `Mul.toSMulMulOpposite` `MulOpposite.op`	—	—
`isSMulRegular_iff_right_eq_zero_of_smul` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsSMulRegular.right_eq_zero_of_smul` `sub_eq_zero` `smul_sub` `sub_self`
`isSMulRegular_map` 📖	mathematical	—	`IsSMulRegular`	—	—
`isSMulRegular_of_group` 📖	mathematical	—	`IsSMulRegular` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`IsScalarTower.left` `inv_mul_cancel` `one_smul`

---

← Back to Index