Documentation Verification Report

Invertible

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

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`, `invertibleNeg`	3
Theorems `neg_mulLeft`, `neg_mulRight`, `neg_mul_eq_mul_neg`, `neg_mul_left`, `neg_mul_neg`, `neg_mul_right`, `val_mulLeft`, `val_mulRight`, `val_neg_mulLeft`, `val_neg_mulRight`, `mul_left`, `mul_right`, `inverse_add_inverse`, `inverse_sub_inverse`, `eq_of_invOf_add_eq_invOf_add_invOf`, `invOf_add_invOf`, `invOf_neg`, `invOf_sub_invOf`, `invOf_two_add_invOf_two`, `neg_add_eq_mul_invOf_mul_same_iff`, `neg_one_eq_invOf_mul_add_invOf_mul_iff`, `one_sub_invOf_two`, `pos_of_invertible_cast`	23
Total	26

AddUnits

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	4 math math: `val_neg_mulLeft`, `val_mulLeft`, `neg_mulLeft`, `neg_mul_left`
`mulRight` 📖	CompOp	4 math math: `val_neg_mulRight`, `neg_mul_right`, `neg_mulRight`, `val_mulRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_mulLeft` 📖	mathematical	—	`AddUnits` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instNeg` `mulLeft`	—	—
`neg_mulRight` 📖	mathematical	—	`AddUnits` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instNeg` `mulRight`	—	—
`neg_mul_eq_mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddUnits` `instNeg`	—	`neg_eq_val_neg` `val_neg_mulRight` `neg_eq_of_add_eq_zero_left` `Distrib.leftDistribClass` `neg_add` `MulZeroClass.mul_zero`
`neg_mul_left` 📖	mathematical	—	`AddUnits` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instNeg` `mulLeft`	—	`neg_mulLeft`
`neg_mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddUnits` `instNeg`	—	`val_mulLeft` `ext_iff` `neg_mulLeft` `neg_neg` `ext` `neg_mul_eq_mul_neg`
`neg_mul_right` 📖	mathematical	—	`AddUnits` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instNeg` `mulRight`	—	`neg_mulRight`
`val_mulLeft` 📖	mathematical	—	`val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`val_mulRight` 📖	mathematical	—	`val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`val_neg_mulLeft` 📖	mathematical	—	`val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddUnits` `instNeg` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `neg`	—	—
`val_neg_mulRight` 📖	mathematical	—	`val` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddUnits` `instNeg` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `neg`	—	—

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_left` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddUnits.isAddUnit`
`mul_right` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddUnits.isAddUnit`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inverse_add_inverse` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `inverse` `Distrib.toMul`	—	`IsUnit.nonempty_invertible` `inverse_invertible` `invOf_add_invOf` `Iff.not` `inverse_non_unit` `add_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`inverse_sub_inverse` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `toAddGroupWithOne` `inverse` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing`	—	`IsUnit.nonempty_invertible` `inverse_invertible` `invOf_sub_invOf` `Iff.not` `inverse_non_unit` `sub_self` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`

(root)

Definitions

Name	Category	Theorems
`invertibleNeg` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_invOf_add_eq_invOf_add_invOf` 📖	—	`Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toAdd`	—	—	`neg_one_eq_invOf_mul_add_invOf_mul_iff` `neg_add_eq_mul_invOf_mul_same_iff` `add_comm`
`invOf_add_invOf` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Invertible.invOf` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_add` `Distrib.leftDistribClass` `invOf_mul_self` `add_mul` `Distrib.rightDistribClass` `one_mul` `mul_assoc` `mul_invOf_self` `mul_one` `add_comm`
`invOf_neg` 📖	mathematical	—	`Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`invOf_eq_right_inv` `mul_neg` `neg_mul` `mul_invOf_self'` `neg_neg`
`invOf_sub_invOf` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mul_sub` `invOf_mul_self` `sub_mul` `one_mul` `mul_assoc` `mul_invOf_self` `mul_one`
`invOf_two_add_invOf_two` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Invertible.invOf` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `mul_invOf_self`
`neg_add_eq_mul_invOf_mul_same_iff` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul` `Invertible.invOf` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`neg_add_rev` `add_neg_cancel_comm` `mul_invOf_self` `one_mul` `mul_assoc` `mul_add` `Distrib.leftDistribClass` `mul_neg` `invOf_mul_self'` `invOf_mul_cancel_left'` `mul_one`
`neg_one_eq_invOf_mul_add_invOf_mul_iff` 📖	mathematical	—	`Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_left_inj_of_invertible` `invOf_mul_self` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `add_comm` `add_assoc` `one_add_one_eq_two` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `neg_add_cancel` `zero_add` `neg_add` `add_zero`
`one_sub_invOf_two` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `isUnit_of_invertible` `mul_sub` `mul_invOf_self` `mul_one` `one_add_one_eq_two` `add_sub_cancel_right`
`pos_of_invertible_cast` 📖	—	—	—	—	`Invertible.ne_zero` `Nat.cast_zero`

---

← Back to Index