Documentation Verification Report

Lemmas

📁 Source: Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `abs_left`, `abs_right`, `add_pow_dvd_pow_of_pow_eq_zero_left`, `add_pow_dvd_pow_of_pow_eq_zero_right`, `pow_dvd_add_pow_of_pow_eq_zero_left`, `pow_dvd_add_pow_of_pow_eq_zero_right`, `pow_dvd_pow_of_add_pow_eq_zero`, `pow_dvd_pow_of_sub_pow_eq_zero`, `pow_dvd_sub_pow_of_pow_eq_zero_left`, `pow_dvd_sub_pow_of_pow_eq_zero_right`, `associated_abs_left_iff`, `associated_abs_right_iff`, `dvd_mul_sub_mul_mul_gcd_of_dvd`, `dvd_mul_sub_mul_mul_left_of_dvd`, `dvd_mul_sub_mul_mul_right_of_dvd`, `dvd_nsmul_of_dvd`, `dvd_smul_of_dvd`, `dvd_zsmul_of_dvd`	18
Total	18

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_left` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`associated_abs_left_iff`
`abs_right` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`associated_abs_right_iff`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow_dvd_pow_of_pow_eq_zero_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`add_pow_dvd_pow_of_pow_eq_zero_right` `symm` `add_comm`
`add_pow_dvd_pow_of_pow_eq_zero_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`pow_dvd_pow_of_sub_pow_eq_zero` `add_left` `add_sub_cancel_right`
`pow_dvd_add_pow_of_pow_eq_zero_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`pow_dvd_add_pow_of_pow_eq_zero_right` `symm` `add_comm`
`pow_dvd_add_pow_of_pow_eq_zero_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`add_pow'` `Finset.dvd_sum` `dvd_nsmul_of_dvd` `le_or_gt` `dvd_mul_of_dvd_left` `pow_dvd_pow` `pow_eq_zero_of_le` `MulZeroClass.mul_zero`
`pow_dvd_pow_of_add_pow_eq_zero` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`neg_neg` `neg_pow'` `dvd_mul_of_dvd_left` `pow_dvd_pow_of_sub_pow_eq_zero` `neg_right` `sub_neg_eq_add`
`pow_dvd_pow_of_sub_pow_eq_zero` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sub_add_cancel` `pow_dvd_add_pow_of_pow_eq_zero_left` `sub_left` `symm` `neg_sub` `neg_pow` `MulZeroClass.mul_zero`
`pow_dvd_sub_pow_of_pow_eq_zero_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`neg_sub` `neg_pow'` `dvd_mul_of_dvd_left` `pow_dvd_sub_pow_of_pow_eq_zero_right` `symm`
`pow_dvd_sub_pow_of_pow_eq_zero_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`pow_dvd_pow_of_sub_pow_eq_zero` `sub_right` `sub_sub_cancel`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_abs_left_iff` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_choice`
`associated_abs_right_iff` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`Associated.comm` `associated_abs_left_iff`
`dvd_mul_sub_mul_mul_gcd_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Distrib.toMul`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	—	`Associated.dvd_iff_dvd_right` `gcd_mul_left'` `dvd_gcd_iff` `dvd_mul_sub_mul_mul_left_of_dvd` `dvd_mul_sub_mul_mul_right_of_dvd`
`dvd_mul_sub_mul_mul_left_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Distrib.toMul`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`dvd_mul_sub_mul_mul_right_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Distrib.toMul`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`dvd_mul_sub_mul_mul_left_of_dvd` `add_comm` `mul_comm`
`dvd_nsmul_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `AddMonoid.toNSMul` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`dvd_smul_of_dvd` `AddMonoid.nat_smulCommClass`
`dvd_smul_of_dvd` 📖	mathematical	`semigroupDvd`	`semigroupDvd`	—	`mul_smul_comm`
`dvd_zsmul_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`dvd_smul_of_dvd` `AddGroup.int_smulCommClass`

---

← Back to Index