Documentation Verification Report

Units

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

Statistics

Metric	Count
Definitions	0
Theorems `addUnits_neg_right`, `addUnits_neg_right_iff`, `addUnits_neg_symm_left`, `addUnits_neg_symm_left_iff`, `addUnits_of_val`, `addUnits_val`, `addUnits_val_iff`, `addUnits_zsmul_right`, `mk_addSemiconjBy`, `units_inv_right`, `units_inv_right_iff`, `units_inv_symm_left`, `units_inv_symm_left_iff`, `units_of_val`, `units_val`, `units_val_iff`, `units_zpow_right`, `conj_pow`, `conj_pow'`, `mk_semiconjBy`	20
Total	20

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addUnits_neg_right` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	`AddUnits` `AddUnits.instNeg`	—	`AddUnits.neg_add_cancel_left` `eq` `add_assoc` `AddUnits.add_neg_cancel_right`
`addUnits_neg_right_iff` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val` `AddUnits` `AddUnits.instNeg`	—	`addUnits_neg_right`
`addUnits_neg_symm_left` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	`AddUnits` `AddUnits.instNeg`	—	`AddUnits.add_neg_cancel_right` `eq` `add_assoc` `AddUnits.neg_add_cancel_left`
`addUnits_neg_symm_left_iff` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val` `AddUnits` `AddUnits.instNeg`	—	`addUnits_neg_symm_left`
`addUnits_of_val` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	`AddUnits` `AddUnits.instAdd`	—	`AddUnits.ext`
`addUnits_val` 📖	mathematical	`AddSemiconjBy` `AddUnits` `AddUnits.instAdd`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	—	—
`addUnits_val_iff` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val` `AddUnits` `AddUnits.instAdd`	—	`addUnits_of_val` `addUnits_val`
`addUnits_zsmul_right` 📖	mathematical	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	`AddUnits` `SubNegMonoid.toZSMul` `AddUnits.instSubNegAddMonoid`	—	`natCast_zsmul` `nsmul_right` `negSucc_zsmul` `addUnits_neg_right`

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_addSemiconjBy` 📖	mathematical	—	`AddSemiconjBy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val` `AddUnits` `instNeg`	—	`neg_add_cancel_right`

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`units_inv_right` 📖	mathematical	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	`Units` `Units.instInv`	—	`Units.inv_mul_cancel_left` `eq` `mul_assoc` `Units.mul_inv_cancel_right`
`units_inv_right_iff` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val` `Units` `Units.instInv`	—	`units_inv_right`
`units_inv_symm_left` 📖	mathematical	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	`Units` `Units.instInv`	—	`Units.mul_inv_cancel_right` `eq` `mul_assoc` `Units.inv_mul_cancel_left`
`units_inv_symm_left_iff` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val` `Units` `Units.instInv`	—	`units_inv_symm_left`
`units_of_val` 📖	mathematical	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	`Units` `Units.instMul`	—	`Units.ext`
`units_val` 📖	mathematical	`SemiconjBy` `Units` `Units.instMul`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	—	—
`units_val_iff` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val` `Units` `Units.instMul`	—	`units_of_val` `units_val`
`units_zpow_right` 📖	mathematical	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	`Units` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`zpow_natCast` `zpow_negSucc`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj_pow` 📖	mathematical	—	`Monoid.toNatPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val` `Units` `instInv`	—	`eq_divp_iff_mul_eq` `SemiconjBy.eq` `SemiconjBy.pow_right` `mk_semiconjBy`
`conj_pow'` 📖	mathematical	—	`Monoid.toNatPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val` `Units` `instInv`	—	`conj_pow`
`mk_semiconjBy` 📖	mathematical	—	`SemiconjBy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val` `Units` `instInv`	—	`inv_mul_cancel_right`

---

← Back to Index