Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Group/Semiconj/Defs.lean

Statistics

Metric	Count
Definitions `AddSemiconjBy`, `SemiconjBy`	2
Theorems `add_left`, `add_right`, `conj_iff`, `conj_mk`, `eq`, `nsmul_right`, `reflexive`, `transitive`, `zero_left`, `zero_right`, `conj_iff`, `conj_mk`, `eq`, `mul_left`, `mul_right`, `one_left`, `one_right`, `pow_right`, `reflexive`, `transitive`, `addSemiconjBy_iff_eq`, `semiconjBy_iff_eq`	22
Total	24

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	—	`AddSemiconjBy` `AddSemigroup.toAdd`	—	—	`add_assoc` `eq`
`add_right` 📖	—	`AddSemiconjBy` `AddSemigroup.toAdd`	—	—	`add_assoc` `eq`
`conj_iff` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toNeg`	—	`add_assoc` `neg_add_cancel_right` `add_left_cancel_iff` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_right_cancel_iff` `AddRightCancelSemigroup.toIsRightCancelAdd`
`conj_mk` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toNeg`	—	`add_assoc` `neg_add_cancel` `add_zero`
`eq` 📖	—	`AddSemiconjBy`	—	—	—
`nsmul_right` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`zero_nsmul` `zero_right` `succ_nsmul` `add_right`
`reflexive` 📖	mathematical	—	`Reflexive` `AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`zero_left`
`transitive` 📖	mathematical	—	`Transitive` `AddSemiconjBy` `AddSemigroup.toAdd`	—	`add_left`
`zero_left` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`zero_right`
`zero_right` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`eq_1` `add_zero` `zero_add`

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj_iff` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toInv`	—	`inv_mul_cancel_right` `mul_assoc` `mul_left_cancel_iff` `LeftCancelSemigroup.toIsLeftCancelMul` `mul_right_cancel_iff` `RightCancelSemigroup.toIsRightCancelMul`
`conj_mk` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toInv`	—	`mul_assoc` `inv_mul_cancel` `mul_one`
`eq` 📖	—	`SemiconjBy`	—	—	—
`mul_left` 📖	—	`SemiconjBy` `Semigroup.toMul`	—	—	`mul_assoc` `eq`
`mul_right` 📖	—	`SemiconjBy` `Semigroup.toMul`	—	—	`mul_assoc` `eq`
`one_left` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`one_right`
`one_right` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`eq_1` `mul_one` `one_mul`
`pow_right` 📖	mathematical	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`pow_zero` `one_right` `pow_succ` `mul_right`
`reflexive` 📖	mathematical	—	`Reflexive` `SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne`	—	`one_left`
`transitive` 📖	mathematical	—	`Transitive` `SemiconjBy` `Semigroup.toMul`	—	`mul_left`

(root)

Definitions

Name	Category	Theorems
`AddSemiconjBy` 📖	MathDef	20 math math: `AddSemiconjBy.addUnits_val_iff`, `AddSemiconjBy.zero_right`, `AddSemiconjBy.addUnits_neg_symm_left_iff`, `addSemiconjBy_map_iff`, `AddSemiconjBy.addUnits_neg_right_iff`, `Prod.addSemiconjBy_iff`, `AddSemiconjBy.neg_symm_left_iff`, `AddSemiconjBy.reflexive`, `AddOpposite.addSemiconjBy_unop`, `AddCommute.addSemiconjBy`, `AddOpposite.addSemiconjBy_op`, `AddSemiconjBy.conj_mk`, `AddSemiconjBy.neg_neg_symm_iff`, `AddSemiconjBy.neg_right_iff`, `addSemiconjBy_iff_eq`, `AddSemiconjBy.zero_left`, `AddUnits.mk_addSemiconjBy`, `AddSemiconjBy.conj_iff`, `AddSemiconjBy.transitive`, `Pi.addSemiconjBy_iff`
`SemiconjBy` 📖	MathDef	30 math math: `Commute.semiconjBy`, `SemiconjBy.inv_inv_symm_iff`, `Prod.semiconjBy_iff`, `SemiconjBy.zero_right`, `semiconjBy_map_iff`, `SemiconjBy.reflexive`, `SemiconjBy.one_right`, `SemiconjBy.neg_one_left`, `SemiconjBy.conj_mk`, `SemiconjBy.units_inv_symm_left_iff`, `SemiconjBy.conj_iff`, `SemiconjBy.inv_symm_left_iff`, `SemiconjBy.inv_right_iff`, `SemiconjBy.zero_left`, `SemiconjBy.neg_left_iff`, `SemiconjBy.neg_right_iff`, `SemiconjBy.units_val_iff`, `SemiconjBy.one_left`, `SemiconjBy.neg_one_right`, `semiconjBy_iff_eq`, `Pi.semiconjBy_iff`, `SemiconjBy.units_inv_right_iff`, `SemiconjBy.inv_symm_left_iff₀`, `MulOpposite.semiconjBy_unop`, `semiconjBy_star_star_star`, `Units.mk_semiconjBy`, `CircleDeg1Lift.semiconjBy_iff_semiconj`, `SemiconjBy.inv_right_iff₀`, `MulOpposite.semiconjBy_op`, `SemiconjBy.transitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSemiconjBy_iff_eq` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid`	—	`add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_comm` `AddSemiconjBy.eq_1`
`semiconjBy_iff_eq` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CancelCommMonoid.toCommMonoid`	—	`mul_left_cancel` `LeftCancelSemigroup.toIsLeftCancelMul` `mul_comm` `SemiconjBy.eq_1`

---

← Back to Index