Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Prime/Defs.lean

Statistics

Metric	Count
Definitions	0
Theorems `dvd_comm`, `dvd_symm`, `ne_zero`, `not_dvd_isUnit`, `not_dvd_one`, `not_dvd_unit`, `prime`, `prime_of_isPrimal`, `dvd_mul`, `dvd_of_dvd_pow`, `dvd_or_dvd`, `dvd_pow_iff_dvd`, `irreducible`, `isPrimal`, `ne_one`, `ne_zero`, `not_dvd_mul`, `not_dvd_one`, `not_unit`, `irreducible_iff_prime`, `not_irreducible_zero`, `not_prime_one`, `not_prime_zero`	23
Total	23

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_comm` 📖	mathematical	`Irreducible`	`semigroupDvd` `Monoid.toSemigroup`	—	`dvd_symm`
`dvd_symm` 📖	—	`Irreducible` `semigroupDvd` `Monoid.toSemigroup`	—	—	`IsUnit.mul_right_dvd` `of_irreducible_mul` `not_isUnit` `dvd_refl`
`ne_zero` 📖	—	`Irreducible` `MonoidWithZero.toMonoid`	—	—	`not_irreducible_zero`
`not_dvd_isUnit` 📖	mathematical	`Irreducible` `CommMonoid.toMonoid` `IsUnit`	`semigroupDvd` `Monoid.toSemigroup`	—	`isUnit_of_dvd_unit` `not_isUnit`
`not_dvd_one` 📖	mathematical	`Irreducible` `CommMonoid.toMonoid`	`semigroupDvd` `Monoid.toSemigroup` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`not_dvd_isUnit` `isUnit_one`
`not_dvd_unit` 📖	mathematical	`Irreducible` `CommMonoid.toMonoid`	`semigroupDvd` `Monoid.toSemigroup` `Units.val`	—	`not_dvd_isUnit` `Units.isUnit`
`prime` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Prime`	—	`prime_of_isPrimal` `DecompositionMonoid.primal`
`prime_of_isPrimal` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `IsPrimal` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`Prime`	—	`ne_zero` `not_isUnit` `IsUnit.mul_right_dvd` `IsUnit.mul_left_dvd` `of_irreducible_mul`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_mul` 📖	mathematical	`Prime`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`dvd_or_dvd` `dvd_mul_of_dvd_left` `dvd_mul_of_dvd_right`
`dvd_of_dvd_pow` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	—	`isUnit_of_dvd_one` `pow_zero` `not_unit` `dvd_or_dvd` `pow_succ'`
`dvd_or_dvd` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	—
`dvd_pow_iff_dvd` 📖	mathematical	`Prime`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`dvd_of_dvd_pow` `dvd_pow`
`irreducible` 📖	mathematical	`Prime`	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`not_unit` `isUnit_of_dvd_one` `mul_dvd_mul_iff_right` `right_ne_zero_of_mul` `ne_zero` `dvd_mul_of_dvd_right` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `left_ne_zero_of_mul` `dvd_mul_of_dvd_left` `dvd_or_dvd` `dvd_rfl`
`isPrimal` 📖	mathematical	`Prime`	`IsPrimal` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`dvd_or_dvd` `one_dvd` `mul_one` `one_mul`
`ne_one` 📖	—	`Prime`	—	—	`isUnit_one`
`ne_zero` 📖	—	`Prime`	—	—	—
`not_dvd_mul` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Iff.not` `dvd_mul`
`not_dvd_one` 📖	mathematical	`Prime`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass`	—	`isUnit_of_dvd_one` `not_unit`
`not_unit` 📖	mathematical	`Prime`	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff_prime` 📖	mathematical	—	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime`	—	`Irreducible.prime` `Prime.irreducible`
`not_irreducible_zero` 📖	mathematical	—	`Irreducible` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`MulZeroClass.mul_zero`
`not_prime_one` 📖	mathematical	—	`Prime` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.not_unit` `isUnit_one`
`not_prime_zero` 📖	mathematical	—	`Prime` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.ne_zero`

---

← Back to Index