Prime

📁 Source: Mathlib/Data/List/Prime.lean

Statistics

Metric	Count
Definitions	0
Theorems dvd_prod_iff, not_dvd_prod, mem_list_primes_of_dvd_prod, perm_of_prod_eq_prod	4
Total	4

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_prod_iff 📖	mathematical	Prime	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	not_dvd_one dvd_or_dvd dvd_trans List.dvd_prod
not_dvd_prod 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	dvd_prod_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_list_primes_of_dvd_prod 📖	—	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—	Prime.dvd_prod_iff prime_dvd_prime_iff_eq
perm_of_prod_eq_prod 📖	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Prime	—	—	dvd_mul_right Prime.not_dvd_one mem_list_primes_of_dvd_prod mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero Prime.ne_zero List.Perm.prod_eq

---

← Back to Index