Lemmas

📁 Source: Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_left, abs_right, add_pow_dvd_pow_of_pow_eq_zero_left, add_pow_dvd_pow_of_pow_eq_zero_right, pow_dvd_add_pow_of_pow_eq_zero_left, pow_dvd_add_pow_of_pow_eq_zero_right, pow_dvd_pow_of_add_pow_eq_zero, pow_dvd_pow_of_sub_pow_eq_zero, pow_dvd_sub_pow_of_pow_eq_zero_left, pow_dvd_sub_pow_of_pow_eq_zero_right, associated_abs_left_iff, associated_abs_right_iff, dvd_mul_sub_mul_mul_gcd_of_dvd, dvd_mul_sub_mul_mul_left_of_dvd, dvd_mul_sub_mul_mul_right_of_dvd, dvd_nsmul_of_dvd, dvd_smul_of_dvd, dvd_zsmul_of_dvd	18
Total	18

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_left 📖	mathematical	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	associated_abs_left_iff
abs_right 📖	mathematical	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	associated_abs_right_iff

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_pow_dvd_pow_of_pow_eq_zero_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Distrib.toAdd	—	add_pow_dvd_pow_of_pow_eq_zero_right symm add_comm
add_pow_dvd_pow_of_pow_eq_zero_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Distrib.toAdd	—	pow_dvd_pow_of_sub_pow_eq_zero add_left add_sub_cancel_right
pow_dvd_add_pow_of_pow_eq_zero_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Distrib.toAdd	—	pow_dvd_add_pow_of_pow_eq_zero_right symm add_comm
pow_dvd_add_pow_of_pow_eq_zero_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Distrib.toAdd	—	add_pow' Finset.dvd_sum dvd_nsmul_of_dvd le_or_gt dvd_mul_of_dvd_left pow_dvd_pow pow_eq_zero_of_le MulZeroClass.mul_zero
pow_dvd_pow_of_add_pow_eq_zero 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring	—	neg_neg neg_pow' dvd_mul_of_dvd_left pow_dvd_pow_of_sub_pow_eq_zero neg_right sub_neg_eq_add
pow_dvd_pow_of_sub_pow_eq_zero 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring	—	sub_add_cancel pow_dvd_add_pow_of_pow_eq_zero_left sub_left symm neg_sub neg_pow MulZeroClass.mul_zero
pow_dvd_sub_pow_of_pow_eq_zero_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	neg_sub neg_pow' dvd_mul_of_dvd_left pow_dvd_sub_pow_of_pow_eq_zero_right symm
pow_dvd_sub_pow_of_pow_eq_zero_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	pow_dvd_pow_of_sub_pow_eq_zero sub_right sub_sub_cancel

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_abs_left_iff 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	abs_choice
associated_abs_right_iff 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Associated.comm associated_abs_left_iff
dvd_mul_sub_mul_mul_gcd_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GCDMonoid.gcd CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	—	Associated.dvd_iff_dvd_right gcd_mul_left' dvd_gcd_iff dvd_mul_sub_mul_mul_left_of_dvd dvd_mul_sub_mul_mul_right_of_dvd
dvd_mul_sub_mul_mul_left_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	—
dvd_mul_sub_mul_mul_right_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	dvd_mul_sub_mul_mul_left_of_dvd add_comm mul_comm
dvd_nsmul_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero	AddMonoid.toNatSMul AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	dvd_smul_of_dvd AddMonoid.nat_smulCommClass
dvd_smul_of_dvd 📖	—	semigroupDvd	—	—	mul_smul_comm
dvd_zsmul_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalRing.toNonUnitalSemiring	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	dvd_smul_of_dvd AddGroup.int_smulCommClass

---

← Back to Index