Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `dvd`	1
Theorems `add`, `linear_comb`, `neg_left`, `neg_right`, `of_neg_left`, `of_neg_right`, `sub`, `dvd_apply`, `decompositionMonoid`, `dvd_add`, `dvd_add_left`, `dvd_add_right`, `dvd_add_self_left`, `dvd_add_self_right`, `dvd_iff_dvd_of_dvd_sub`, `dvd_mul_sub_mul`, `dvd_neg`, `dvd_sub`, `dvd_sub_comm`, `dvd_sub_left`, `dvd_sub_right`, `dvd_sub_self_left`, `dvd_sub_self_right`, `map_dvd_iff`, `map_dvd_iff_dvd_symm`, `min_pow_dvd_add`, `neg_dvd`	27
Total	28

Dvd.dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`semigroupDvd`	—	—	`dvd_add`
`linear_comb` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	`dvd_add` `Distrib.leftDistribClass` `mul_left`
`neg_left` 📖	mathematical	`semigroupDvd`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	`neg_dvd`
`neg_right` 📖	mathematical	`semigroupDvd`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	`dvd_neg`
`of_neg_left` 📖	—	`semigroupDvd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	—	`neg_dvd`
`of_neg_right` 📖	—	`semigroupDvd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	—	`dvd_neg`
`sub` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`dvd_sub`

Equiv

Definitions

Name	Category	Theorems
`dvd` 📖	CompOp	1 math math: `dvd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_apply` 📖	mathematical	—	`semigroupDvd` `LeftCancelSemigroup.toSemigroup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `dvd` `Semigroup.toMul`	—	—

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompositionMonoid` 📖	mathematical	—	`DecompositionMonoid`	—	`DecompositionMonoid.primal` `map_mul` `MulEquivClass.instMulHomClass` `map_dvd_iff` `instMulEquivClass` `apply_symm_apply`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_add` 📖	—	`semigroupDvd`	—	—	`Dvd.elim` `Dvd.intro` `left_distrib`
`dvd_add_left` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`add_sub_cancel_right` `dvd_sub` `dvd_add` `Distrib.leftDistribClass`
`dvd_add_right` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`add_comm` `dvd_add_left`
`dvd_add_self_left` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`dvd_add_right` `dvd_refl`
`dvd_add_self_right` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`dvd_add_left` `dvd_refl`
`dvd_iff_dvd_of_dvd_sub` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	—	`sub_add_cancel` `dvd_add_right`
`dvd_mul_sub_mul` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`mul_sub_left_distrib` `mul_sub_right_distrib` `sub_eq_add_neg` `add_assoc` `neg_add_cancel_left` `dvd_add` `Distrib.leftDistribClass` `Dvd.dvd.mul_left` `Dvd.dvd.mul_right`
`dvd_neg` 📖	mathematical	—	`semigroupDvd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	`Equiv.exists_congr_left` `mul_neg`
`dvd_sub` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`Dvd.dvd.add` `Distrib.leftDistribClass` `Dvd.dvd.neg_right`
`dvd_sub_comm` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`dvd_neg` `neg_sub`
`dvd_sub_left` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`dvd_add_left` `dvd_neg`
`dvd_sub_right` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalRing.toNonUnitalSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`sub_eq_add_neg` `dvd_add_right` `dvd_neg`
`dvd_sub_self_left` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`dvd_sub_right` `dvd_rfl`
`dvd_sub_self_right` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`dvd_sub_left` `dvd_rfl`
`map_dvd_iff` 📖	mathematical	—	`semigroupDvd` `DFunLike.coe` `EquivLike.toFunLike`	—	`Equiv.left_inv` `map_dvd` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass`
`map_dvd_iff_dvd_symm` 📖	mathematical	—	`semigroupDvd` `DFunLike.coe` `EquivLike.toFunLike` `MulEquiv` `Semigroup.toMul` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv`	—	`EquivLike.surjective` `MulEquivClass.coe_symm_apply_apply`
`min_pow_dvd_add` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Dvd.dvd.add` `Distrib.leftDistribClass` `Dvd.dvd.trans` `pow_dvd_pow`
`neg_dvd` 📖	mathematical	—	`semigroupDvd` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `Semigroup.toMul`	—	`Equiv.exists_congr_left` `mul_neg` `neg_mul` `neg_neg`

---

← Back to Index