Divisibility

📁 Source: Mathlib/Algebra/GroupWithZero/Divisibility.lean

Statistics

Metric	Count
Definitions DvdNotUnit	1
Theorems antisymm, antisymm', dvd_iff, mul, ne_zero_or_ne_zero, dvdNotUnit_of_dvd_of_not_dvd, dvd_and_not_dvd_iff, dvd_antisymm, dvd_antisymm', dvd_zero, eq_of_forall_dvd, eq_of_forall_dvd', eq_zero_of_zero_dvd, isPrimal_zero, isRelPrime_of_no_nonunits_factors, isRelPrime_zero_left, isRelPrime_zero_right, mul_dvd_mul_iff_left, mul_dvd_mul_iff_right, ne_zero_of_dvd_ne_zero, not_isRelPrime_zero_zero, pow_dvd_pow_iff, zero_dvd_iff	23
Total	24

Dvd.dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	dvd_antisymm
antisymm' 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	dvd_antisymm'

GroupWithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	MulZeroClass.zero_mul eq_or_ne MulZeroClass.mul_zero mul_inv_cancel_left₀

IsPrimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul 📖	mathematical	IsPrimal SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	eq_or_ne MulZeroClass.zero_mul dvd_of_mul_right_dvd mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero mul_mul_mul_comm mul_dvd_mul_left

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne_zero_or_ne_zero 📖	—	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	—	not_or_of_imp not_isRelPrime_zero_zero

(root)

Definitions

Name	Category	Theorems
DvdNotUnit 📖	MathDef	12 math math: Associates.mk_dvdNotUnit_mk_iff, wellFounded_dvdNotUnit, Associates.dvdNotUnit_of_lt, dvd_and_not_dvd_iff, Nat.dvdNotUnit_setGcd_insert, Valuation.Integers.dvdNotUnit_iff_lt, Associates.dvdNotUnit_iff_lt, dvdNotUnit_of_dvd_of_not_dvd, Ideal.span_singleton_lt_span_singleton, Ideal.dvdNotUnit_iff_lt, UniqueFactorizationMonoid.toIsWellFounded, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvdNotUnit_of_dvd_of_not_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	DvdNotUnit	—	dvd_zero
dvd_and_not_dvd_iff 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero DvdNotUnit	—	isUnit_iff_dvd_one mul_assoc mul_one isUnit_of_dvd_one mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero
dvd_antisymm 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	mul_eq_one mul_right_eq_self₀ IsCancelMulZero.toIsLeftCancelMulZero mul_assoc mul_one MulZeroClass.zero_mul
dvd_antisymm' 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	dvd_antisymm
dvd_zero 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MulZeroClass.toZero SemigroupWithZero.toMulZeroClass	—	Dvd.intro MulZeroClass.mul_zero
eq_of_forall_dvd 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	Dvd.dvd.antisymm dvd_rfl
eq_of_forall_dvd' 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero	—	—	Dvd.dvd.antisymm dvd_rfl
eq_zero_of_zero_dvd 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MulZeroClass.toZero SemigroupWithZero.toMulZeroClass	—	—	Dvd.elim MulZeroClass.zero_mul
isPrimal_zero 📖	mathematical	—	IsPrimal SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	dvd_rfl zero_dvd_iff
isRelPrime_of_no_nonunits_factors 📖	mathematical	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero	IsRelPrime MonoidWithZero.toMonoid	—	by_contra zero_dvd_iff
isRelPrime_zero_left 📖	mathematical	—	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsUnit	—	dvd_zero dvd_rfl IsUnit.isRelPrime_right
isRelPrime_zero_right 📖	mathematical	—	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsUnit	—	isRelPrime_comm isRelPrime_zero_left
mul_dvd_mul_iff_left 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	mul_assoc mul_right_inj'
mul_dvd_mul_iff_right 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	mul_right_comm mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero
ne_zero_of_dvd_ne_zero 📖	—	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero	—	—	left_ne_zero_of_mul
not_isRelPrime_zero_zero 📖	mathematical	—	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	isRelPrime_zero_right not_isUnit_zero
pow_dvd_pow_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero Monoid.toNatPow	—	not_lt pow_succ mul_one Dvd.dvd.trans pow_dvd_pow isUnit_iff_dvd_one mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero pow_ne_zero isReduced_of_noZeroDivisors IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero
zero_dvd_iff 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup MulZeroClass.toZero SemigroupWithZero.toMulZeroClass	—	eq_zero_of_zero_dvd MulZeroClass.mul_zero

---

← Back to Index