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 MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	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 📖	mathematical	IsRelPrime DFunLike.coe	IsRelPrime	—	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 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	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 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	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 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid	—	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 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid	—	pow_dvd_of_dvd_mul_left mul_comm

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_prime 📖	mathematical	DFunLike.coe Prime	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 MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	DvdNotUnit.isUnit_of_irreducible_right
not_prime_pow 📖	mathematical	—	Prime Monoid.toPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	not_irreducible_pow Prime.irreducible
pow_inj_of_not_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	Monoid.toPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	pow_injective_of_not_isUnit
pow_injective_of_not_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	Monoid.toPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	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 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid	—	Prime.pow_dvd_of_dvd_mul_right
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul 📖	mathematical	Prime semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero Monoid.toPow MonoidWithZero.toMonoid	—	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