Documentation Verification Report

Associator

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

Statistics

Metric	Count
Definitions `associator`, `mulLeft₃`, `mulRight₃`, `associator`	4
Theorems `associator_apply`, `associator_eq_zero`, `associator_eq_zero_iff_associative`, `mulLeft₃_apply`, `mulLeft₃_eq_mulRight₃`, `mulLeft₃_eq_mulRight₃_iff_associative`, `mulRight₃_apply`, `associator_apply`, `associator_cocycle`, `associator_eq_zero`, `associator_eq_zero_iff_associative`, `associator_op`	12
Total	16

AddMonoidHom

Definitions

Name	Category	Theorems
`associator` 📖	CompOp	3 math math: `associator_apply`, `associator_eq_zero_iff_associative`, `associator_eq_zero`
`mulLeft₃` 📖	CompOp	3 math math: `mulLeft₃_eq_mulRight₃`, `mulLeft₃_apply`, `mulLeft₃_eq_mulRight₃_iff_associative`
`mulRight₃` 📖	CompOp	3 math math: `mulLeft₃_eq_mulRight₃`, `mulLeft₃_eq_mulRight₃_iff_associative`, `mulRight₃_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `instFunLike` `instAddCommGroup` `associator` `associator`	—	—
`associator_eq_zero` 📖	mathematical	—	`associator` `NonUnitalRing.toNonUnitalNonAssocRing` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `instAddCommGroup` `instZeroAddMonoidHom`	—	`associator_eq_zero_iff_associative` `Semigroup.to_isAssociative`
`associator_eq_zero_iff_associative` 📖	mathematical	—	`associator` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `instAddCommGroup` `instZeroAddMonoidHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`mulLeft₃_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instAddCommMonoid` `mulLeft₃` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulLeft₃_eq_mulRight₃` 📖	mathematical	—	`mulLeft₃` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `mulRight₃`	—	`mulLeft₃_eq_mulRight₃_iff_associative` `Semigroup.to_isAssociative`
`mulLeft₃_eq_mulRight₃_iff_associative` 📖	mathematical	—	`mulLeft₃` `mulRight₃` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mulLeft₃_apply` `mulRight₃_apply` `ext`
`mulRight₃_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instAddCommMonoid` `mulRight₃` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

(root)

Definitions

Name	Category	Theorems
`associator` 📖	CompOp	11 math math: `associator_apply`, `LeftPreLieRing.assoc_symm'`, `associator_op`, `LeftPreLieRing.assoc_symm`, `AddMonoidHom.associator_apply`, `associator_eq_zero_iff_associative`, `associator_cocycle`, `LieAdmissibleRing.assoc_def`, `RightPreLieRing.assoc_symm'`, `RightPreLieRing.assoc_symm`, `associator_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_apply` 📖	mathematical	—	`associator` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`associator_cocycle` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `associator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_sub` `sub_mul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg`
`associator_eq_zero` 📖	mathematical	—	`associator` `NonUnitalRing.toNonUnitalNonAssocRing` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`associator_eq_zero_iff_associative` `Semigroup.to_isAssociative`
`associator_eq_zero_iff_associative` 📖	mathematical	—	`associator` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sub_eq_zero` `sub_self`
`associator_op` 📖	mathematical	—	`associator` `MulOpposite` `MulOpposite.instNonUnitalNonAssocRing` `MulOpposite.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `MulOpposite.op` `MulOpposite.unop`	—	`neg_sub`

---

← Back to Index