Basic

📁 Source: Mathlib/Algebra/Ring/Basic.lean

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`, `mulLeft`, `mulRight`, `mul`, `mulLeft`, `mulRight`, `instHasDistribNeg`	8
Theorems `mulLeft_apply`, `mulRight_apply`, `mulLeft_apply_apply`, `mulRight_apply_apply`, `mulRight_eq_mulLeft`, `coe_flip_mul`, `coe_mul`, `coe_mulLeft`, `coe_mulRight`, `map_mul_iff`, `mulLeft_eq_mulRight_iff_forall_commute`, `mulRight_apply`, `mulRight_eq_mulLeft_iff_forall_commute`, `mul_apply`, `to_noZeroDivisors`, `to_isCancelMulZero`, `to_isDomain`, `to_isCancelMulZero`, `to_noZeroDivisors`, `div_neg`, `div_neg_eq_neg_div`, `div_neg_eq_neg_div'`, `inv_neg`, `inv_neg_one`, `isCancelMulZero_iff_isDomain_or_subsingleton`, `isCancelMulZero_iff_noZeroDivisors`, `isDomain_iff_cancelMulZero_and_nontrivial`, `isDomain_iff_noZeroDivisors_and_nontrivial`, `isLeftRegular_iff_right_eq_zero_of_mul`, `isRegular_iff_eq_zero_of_mul`, `isRightRegular_iff_left_eq_zero_of_mul`, `neg_div`, `neg_div'`, `neg_div_neg_eq`, `neg_inv`, `noZeroDivisors_iff_isDomain_or_subsingleton`, `noZeroDivisors_tfae`, `one_div_neg_eq_neg_one_div`, `one_div_neg_one_eq_neg_one`, `pred_ne_self`, `succ_ne_self`, `vieta_formula_quadratic`	42
Total	50

AddHom

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	1 math math: `mulLeft_apply`
`mulRight` 📖	CompOp	1 math math: `mulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `Distrib.toAdd` `funLike` `mulLeft` `Distrib.toMul`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `Distrib.toAdd` `funLike` `mulRight` `Distrib.toMul`	—	—

AddMonoid.End

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	11 math math: `mulRight_eq_mulLeft`, `commute_lmul_rmul`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `two_nsmul_lie_lmul_lmul_add_add_eq_zero`, `commute_lmul_sq_rmul`, `commute_lmul_rmul_sq`, `mulLeft_apply_apply`, `NonUnitalNonAssocCommSemiring.mem_center_iff`, `commute_lmul_lmul_sq`, `two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add`, `NonUnitalNonAssocSemiring.mem_center_iff`
`mulRight` 📖	CompOp	8 math math: `mulRight_apply_apply`, `mulRight_eq_mulLeft`, `commute_lmul_rmul`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `commute_lmul_sq_rmul`, `commute_lmul_rmul_sq`, `NonUnitalNonAssocSemiring.mem_center_iff`, `commute_rmul_rmul_sq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoid.End` `instAddCommMonoid` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulRight_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoid.End` `instAddCommMonoid` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulRight_eq_mulLeft` 📖	mathematical	—	`mulRight` `NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring` `mulLeft`	—	`AddMonoidHom.ext` `AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute` `Commute.all`

AddMonoidHom

Definitions

Name	Category	Theorems
`mul` 📖	CompOp	5 math math: `coe_flip_mul`, `Set.mem_center_iff_addMonoidHom`, `mul_apply`, `coe_mul`, `map_mul_iff`
`mulLeft` 📖	CompOp	9 math math: `LinearMap.toAddMonoidHom_mulLeft`, `Set.mem_center_iff_addMonoidHom`, `mulLeft_continuous`, `mulRight_eq_mulLeft_iff_forall_commute`, `coe_mul`, `coe_mulLeft`, `mulLeft_eq_mulRight_iff_forall_commute`, `mulLeft_bound`, `LinearMap.mulLeft_toAddMonoidHom`
`mulRight` 📖	CompOp	10 math math: `coe_flip_mul`, `mulRight_bound`, `Set.mem_center_iff_addMonoidHom`, `mulRight_apply`, `mulRight_continuous`, `mulRight_eq_mulLeft_iff_forall_commute`, `coe_mulRight`, `LinearMap.mulRight_toAddMonoidHom`, `LinearMap.toAddMonoidHom_mulRight`, `mulLeft_eq_mulRight_iff_forall_commute`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_flip_mul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instAddCommMonoid` `instFunLike` `flip` `mul` `mulRight`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instAddCommMonoid` `instFunLike` `mul` `mulLeft`	—	—
`coe_mulLeft` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coe_mulRight` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`map_mul_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `compr₂` `mul` `compl₂` `comp` `instAddCommMonoid`	—	`ext_iff₂`
`mulLeft_eq_mulRight_iff_forall_commute` 📖	mathematical	—	`mulLeft` `mulRight` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`DFunLike.ext_iff`
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulRight_eq_mulLeft_iff_forall_commute` 📖	mathematical	—	`mulRight` `mulLeft` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`DFunLike.ext_iff`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instAddCommMonoid` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_noZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero`

MulOpposite

Definitions

Name	Category	Theorems
`instHasDistribNeg` 📖	CompOp	—

NoZeroDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`isCancelMulZero_iff_noZeroDivisors`
`to_isDomain` 📖	mathematical	—	`IsDomain` `Ring.toSemiring`	—	`to_isCancelMulZero`

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isCancelMulZero` 📖	mathematical	—	`IsCancelMulZero`	—	`eq_zero`
`to_noZeroDivisors` 📖	mathematical	—	`NoZeroDivisors`	—	`eq_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_neg` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_neg_eq_neg_div`
`div_neg_eq_neg_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`inv_eq_one_div` `division_def` `one_div_neg_eq_neg_one_div` `neg_mul_eq_mul_neg` `mul_one_div`
`div_neg_eq_neg_div'` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_neg` `neg_div`
`inv_neg` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	—	`neg_inv`
`inv_neg_one` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toOne`	—	`neg_inv` `inv_one`
`isCancelMulZero_iff_isDomain_or_subsingleton` 📖	mathematical	—	`IsCancelMulZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsDomain`	—	`not_subsingleton_iff_nontrivial` `IsDomain.toIsCancelMulZero` `Subsingleton.to_isCancelMulZero`
`isCancelMulZero_iff_noZeroDivisors` 📖	mathematical	—	`IsCancelMulZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NoZeroDivisors`	—	`List.TFAE.out` `noZeroDivisors_tfae`
`isDomain_iff_cancelMulZero_and_nontrivial` 📖	mathematical	—	`IsDomain` `IsCancelMulZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nontrivial`	—	`IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial`
`isDomain_iff_noZeroDivisors_and_nontrivial` 📖	mathematical	—	`IsDomain` `Ring.toSemiring` `NoZeroDivisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nontrivial`	—	`isCancelMulZero_iff_noZeroDivisors` `isDomain_iff_cancelMulZero_and_nontrivial`
`isLeftRegular_iff_right_eq_zero_of_mul` 📖	mathematical	—	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`MulZeroClass.mul_zero` `sub_eq_zero` `mul_sub` `sub_self`
`isRegular_iff_eq_zero_of_mul` 📖	mathematical	—	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`isRegular_iff` `isLeftRegular_iff_right_eq_zero_of_mul` `isRightRegular_iff_left_eq_zero_of_mul`
`isRightRegular_iff_left_eq_zero_of_mul` 📖	mathematical	—	`IsRightRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`MulZeroClass.zero_mul` `sub_eq_zero` `sub_mul` `sub_self`
`neg_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`neg_eq_neg_one_mul` `mul_div_assoc`
`neg_div'` 📖	mathematical	—	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivInvMonoid.toDiv`	—	`neg_div`
`neg_div_neg_eq` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_neg_eq_neg_div` `neg_div` `neg_neg`
`neg_inv` 📖	mathematical	—	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`inv_eq_one_div` `div_neg_eq_neg_div`
`noZeroDivisors_iff_isDomain_or_subsingleton` 📖	mathematical	—	`NoZeroDivisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsDomain` `Ring.toSemiring`	—	`isCancelMulZero_iff_noZeroDivisors` `isCancelMulZero_iff_isDomain_or_subsingleton`
`noZeroDivisors_tfae` 📖	mathematical	—	`List.TFAE` `NoZeroDivisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsLeftCancelMulZero` `IsRightCancelMulZero` `IsCancelMulZero`	—	`noZeroDivisors_iff_right_eq_zero_of_mul` `noZeroDivisors_iff_left_eq_zero_of_mul` `noZeroDivisors_iff_eq_zero_of_mul` `List.tfae_of_cycle`
`one_div_neg_eq_neg_one_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`neg_eq_neg_one_mul` `one_div_mul_one_div_rev` `one_div_neg_one_eq_neg_one` `mul_neg` `mul_one`
`one_div_neg_one_eq_neg_one` 📖	mathematical	—	`DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`neg_mul_neg` `one_mul` `eq_one_div_of_mul_eq_one_right`
`pred_ne_self` 📖	—	—	—	—	`one_ne_zero` `NeZero.one` `neg_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `neg_zero` `add_zero`
`succ_ne_self` 📖	—	—	—	—	`one_ne_zero` `NeZero.one` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_zero`
`vieta_formula_quadratic` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`eq_neg_of_add_eq_zero_right` `neg_sub` `mul_sub` `mul_comm` `sub_add` `sub_mul` `sub_self` `add_sub_cancel`

---

← Back to Index