Documentation Verification Report

Defs

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

Statistics

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

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addConj_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`
`addConj_mk` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toNeg`	—	`add_assoc` `neg_add_cancel` `add_zero`
`add_left` 📖	mathematical	`AddSemiconjBy` `AddSemigroup.toAdd`	`AddSemiconjBy` `AddSemigroup.toAdd`	—	`add_assoc` `eq`
`add_right` 📖	mathematical	`AddSemiconjBy` `AddSemigroup.toAdd`	`AddSemiconjBy` `AddSemigroup.toAdd`	—	`add_assoc` `eq`
`eq` 📖	—	`AddSemiconjBy`	—	—	—
`isTrans` 📖	mathematical	—	`IsTrans` `AddSemiconjBy` `AddSemigroup.toAdd`	—	`add_left`
`nsmul_right` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`zero_nsmul` `zero_right` `succ_nsmul` `add_right`
`reflexive` 📖	mathematical	—	`Reflexive` `AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`zero_left`
`transitive` 📖	mathematical	—	`IsTrans` `AddSemiconjBy` `AddSemigroup.toAdd`	—	`isTrans`
`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`	—	—	—
`isTrans` 📖	mathematical	—	`IsTrans` `SemiconjBy` `Semigroup.toMul`	—	`mul_left`
`mul_left` 📖	mathematical	`SemiconjBy` `Semigroup.toMul`	`SemiconjBy` `Semigroup.toMul`	—	`mul_assoc` `eq`
`mul_right` 📖	mathematical	`SemiconjBy` `Semigroup.toMul`	`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`	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_zero` `one_right` `pow_succ` `mul_right`
`reflexive` 📖	mathematical	—	`Reflexive` `SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne`	—	`one_left`
`transitive` 📖	mathematical	—	`IsTrans` `SemiconjBy` `Semigroup.toMul`	—	`isTrans`

(root)

Definitions

Name	Category	Theorems
`AddSemiconjBy` 📖	MathDef	39 math math: `AddSemiconjBy.addUnits_val_iff`, `AddSemiconjBy.addConj_mk`, `AddSemiconjBy.addUnits_neg_right`, `AddSemiconjBy.addUnits_val`, `AddSemiconjBy.zero_right`, `AddSemiconjBy.neg_right`, `AddSemiconjBy.nsmul_right`, `AddSemiconjBy.addUnits_neg_symm_left_iff`, `addSemiconjBy_map_iff`, `AddSemiconjBy.addUnits_neg_right_iff`, `AddSemiconjBy.of_map`, `Prod.addSemiconjBy_iff`, `AddSemiconjBy.neg_symm_left_iff`, `AddSemiconjBy.map`, `AddSemiconjBy.reflexive`, `AddSemiconjBy.add_right`, `AddOpposite.addSemiconjBy_unop`, `AddSemiconjBy.add_left`, `AddSemiconjBy.prod`, `AddSemiconjBy.addUnits_zsmul_right`, `AddCommute.addSemiconjBy`, `AddSemiconjBy.neg_symm_left`, `AddOpposite.addSemiconjBy_op`, `AddSemiconjBy.neg_neg_symm_iff`, `AddSemiconjBy.neg_right_iff`, `AddSemiconjBy.zsmul_right`, `AddSemiconjBy.addConj_iff`, `addSemiconjBy_iff_eq`, `AddSemiconjBy.addUnits_of_val`, `AddSemiconjBy.op`, `AddSemiconjBy.zero_left`, `AddUnits.mk_addSemiconjBy`, `AddSemiconjBy.unop`, `AddSemiconjBy.neg_neg_symm`, `AddSemiconjBy.transitive`, `AddSemiconjBy.isTrans`, `Pi.addSemiconjBy_iff`, `AddSemiconjBy.addUnits_neg_symm_left`, `AddSemiconjBy.pi`
`SemiconjBy` 📖	MathDef	69 math math: `Commute.semiconjBy`, `SemiconjBy.unop`, `Matrix.SemiconjBy.zpow_right`, `SemiconjBy.inv_inv_symm_iff`, `Prod.semiconjBy_iff`, `SemiconjBy.div_right`, `SemiconjBy.prod`, `SemiconjBy.tprod`, `SemiconjBy.inv_right₀`, `SemiconjBy.inv_inv_symm`, `SemiconjBy.zero_right`, `SemiconjBy.intCast_mul_right`, `SemiconjBy.tmul`, `semiconjBy_map_iff`, `SemiconjBy.isTrans`, `SemiconjBy.inv_right`, `SemiconjBy.zpow_right₀`, `SemiconjBy.natCast_mul_right`, `SemiconjBy.of_map`, `SemiconjBy.reflexive`, `SemiconjBy.one_right`, `SemiconjBy.add_left`, `SemiconjBy.natCast_mul_left`, `SemiconjBy.intCast_mul_left`, `SemiconjBy.pow_right`, `SemiconjBy.neg_one_left`, `SemiconjBy.sub_left`, `SemiconjBy.inv_symm_left₀`, `SemiconjBy.sub_right`, `SemiconjBy.inv_symm_left`, `SemiconjBy.star_star_star`, `SemiconjBy.add_right`, `SemiconjBy.conj_mk`, `SemiconjBy.map`, `SemiconjBy.units_inv_symm_left_iff`, `SemiconjBy.mul_right`, `SemiconjBy.conj_iff`, `SemiconjBy.inv_symm_left_iff`, `SemiconjBy.units_of_val`, `SemiconjBy.neg_right`, `SemiconjBy.inv_right_iff`, `SemiconjBy.zero_left`, `SemiconjBy.neg_left_iff`, `SemiconjBy.neg_right_iff`, `SemiconjBy.zpow_right`, `SemiconjBy.units_zpow_right`, `SemiconjBy.units_val_iff`, `SemiconjBy.intCast_mul_intCast_mul`, `SemiconjBy.one_left`, `SemiconjBy.op`, `SemiconjBy.neg_one_right`, `semiconjBy_iff_eq`, `SemiconjBy.units_inv_symm_left`, `SemiconjBy.natCast_mul_natCast_mul`, `SemiconjBy.neg_left`, `Pi.semiconjBy_iff`, `SemiconjBy.units_val`, `SemiconjBy.mul_left`, `SemiconjBy.units_inv_right_iff`, `SemiconjBy.units_inv_right`, `SemiconjBy.inv_symm_left_iff₀`, `MulOpposite.semiconjBy_unop`, `semiconjBy_star_star_star`, `Units.mk_semiconjBy`, `SemiconjBy.pi`, `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