Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `isUnit_of_irreducible_right`, `ne`, `not_unit`, `of_map`, `not_prime`, `prime_iff`, `dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd`, `left_dvd_or_dvd_right_of_dvd_mul`, `not_isSquare`, `pow_dvd_of_dvd_mul_left`, `pow_dvd_of_dvd_mul_right`, `comap_prime`, `not_irreducible_of_not_unit_dvdNotUnit`, `not_prime_pow`, `pow_inj_of_not_isUnit`, `pow_injective_of_not_isUnit`, `prime_pow_succ_dvd_mul`, `succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul`	18
Total	18

DvdNotUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_of_irreducible_right` 📖	mathematical	`DvdNotUnit` `Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`IsUnit`	—	`irreducible_iff`
`ne` 📖	—	`DvdNotUnit`	—	—	`IsCancelMulZero.toIsLeftCancelMulZero`
`not_unit` 📖	mathematical	`DvdNotUnit`	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`isUnit_iff_dvd_one` `dvd_of_mul_left_dvd`

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_map` 📖	—	`IsRelPrime` `DFunLike.coe`	—	—	`IsUnit.of_map` `map_dvd`

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_prime` 📖	mathematical	`IsSquare` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Prime`	—	`Prime.not_isSquare`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prime_iff` 📖	mathematical	—	`Prime` `DFunLike.coe` `EquivLike.toFunLike`	—	`comap_prime` `MulEquivClass.toMonoidWithZeroHomClass` `instMulEquivClass` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `symm_apply_apply` `apply_symm_apply`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`dvd_or_dvd` `Dvd.dvd.trans` `dvd_pow_self` `dvd_of_dvd_pow` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `ne_zero` `mul_assoc` `pow_succ` `mul_pow` `mul_comm` `pow_two` `dvd_mul_right`
`left_dvd_or_dvd_right_of_dvd_mul` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`dvd_mul_right` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `ne_zero` `mul_left_comm`
`not_isSquare` 📖	mathematical	`Prime`	`IsSquare` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`Irreducible.not_isSquare` `irreducible`
`pow_dvd_of_dvd_mul_left` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`pow_zero` `one_dvd` `dvd_trans` `pow_dvd_pow` `pow_succ` `mul_dvd_mul_left` `dvd_or_dvd` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `ne_zero` `mul_left_comm`
`pow_dvd_of_dvd_mul_right` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`pow_dvd_of_dvd_mul_left` `mul_comm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_prime` 📖	—	`DFunLike.coe` `Prime`	—	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `map_dvd` `map_mul` `MonoidHomClass.toMulHomClass`
`not_irreducible_of_not_unit_dvdNotUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `DvdNotUnit`	`Irreducible`	—	`DvdNotUnit.isUnit_of_irreducible_right`
`not_prime_pow` 📖	mathematical	—	`Prime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`not_irreducible_pow` `Prime.irreducible`
`pow_inj_of_not_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Monoid.toNatPow`	—	`pow_injective_of_not_isUnit`
`pow_injective_of_not_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Monoid.toNatPow`	—	`Function.Injective.of_lt_imp_ne` `DvdNotUnit.ne` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `not_isUnit_of_not_isUnit_dvd` `dvd_pow` `dvd_refl` `LT.lt.ne'` `pow_mul_pow_sub` `LT.lt.le`
`prime_pow_succ_dvd_mul` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`Prime.pow_dvd_of_dvd_mul_right`
`succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`pow_add` `mul_comm` `mul_assoc` `mul_left_comm` `pow_one` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `Prime.ne_zero` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Prime.dvd_or_dvd` `pow_succ`

---

← Back to Index