Basic

📁 Source: Mathlib/Algebra/EuclideanDomain/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems add_mul_div_left, add_mul_div_right, div_add_div_of_dvd, div_div, div_dvd_of_dvd, div_eq_div_iff_mul_eq_mul_of_dvd, div_eq_iff_eq_mul_of_dvd, div_mul, div_one, div_pow, div_self, div_sub_div_of_dvd, dvd_div_of_mul_dvd, dvd_gcd, dvd_lcm_left, dvd_lcm_right, dvd_mod_iff, eq_div_iff_mul_eq_of_dvd, eq_div_of_mul_eq_left, eq_div_of_mul_eq_right, gcd_dvd, gcd_dvd_left, gcd_dvd_right, gcd_eq_gcd_ab, gcd_eq_left, gcd_eq_zero_iff, gcd_mul_lcm, gcd_one_left, gcd_self, gcd_val, gcd_zero_right, instIsDomain, lcm_dvd, lcm_dvd_iff, lcm_eq_zero_iff, lcm_zero_left, lcm_zero_right, mod_eq_sub_mul_div, mod_eq_zero, mod_one, mod_self, mul_add_div_left, mul_add_div_right, mul_div_assoc, mul_div_cancel', mul_div_mul_cancel, mul_div_mul_comm_of_dvd_dvd, mul_sub_div_left, mul_sub_div_right, sub_mul_div_left, sub_mul_div_right, toMulDivCancelClass, val_dvd_le, xgcdAux_P, xgcdAux_fst, xgcdAux_val, zero_div, zero_mod	58
Total	58

EuclideanDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mul_div_left 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	—	eq_div_of_mul_eq_right mul_add Distrib.leftDistribClass mul_div_cancel'
add_mul_div_right 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	—	mul_comm add_mul_div_left
div_add_div_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instDiv Distrib.toMul	—	eq_div_of_mul_eq_right mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain mul_add Distrib.leftDistribClass mul_assoc mul_div_cancel' mul_comm
div_div 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing instDiv	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	eq_or_ne div_zero zero_div MulZeroClass.zero_mul div_mul mul_div_cancel' mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
div_dvd_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv	—	zero_dvd_iff dvd_zero mul_comm mul_div_assoc mul_div_cancel_right₀ toMulDivCancelClass
div_eq_div_iff_mul_eq_mul_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	div_eq_iff_eq_mul_of_dvd mul_div_assoc eq_div_iff_mul_eq_of_dvd mul_comm mul_assoc
div_eq_iff_eq_mul_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	mul_div_cancel_left₀ toMulDivCancelClass IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
div_mul 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	instDiv	—	eq_or_ne MulZeroClass.mul_zero div_zero eq_div_of_mul_eq_right mul_div_assoc mul_comm mul_div_mul_cancel
div_one 📖	mathematical	—	instDiv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toCommRing	—	eq_div_of_mul_eq_left one_ne_zero' NeZero.one toNontrivial mul_one
div_pow 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instDiv	—	eq_or_ne MulZeroClass.zero_mul div_zero pow_zero div_self NeZero.one toNontrivial zero_pow mul_div_cancel_left₀ toMulDivCancelClass mul_pow isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
div_self 📖	mathematical	—	instDiv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toCommRing	—	one_mul mul_div_cancel_right₀ toMulDivCancelClass
div_sub_div_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	eq_div_of_mul_eq_right mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain mul_sub mul_assoc mul_div_cancel' mul_comm
dvd_div_of_mul_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	instDiv	—	eq_or_ne div_zero mul_assoc mul_div_cancel_left₀ toMulDivCancelClass
dvd_gcd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	gcd	—	GCD.induction gcd_zero_left gcd_val dvd_mod_iff
dvd_lcm_left 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing lcm	—	by_cases lcm.eq_1 div_zero dvd_zero gcd_dvd eq_div_of_mul_eq_left mul_right_comm mul_assoc
dvd_lcm_right 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing lcm	—	by_cases lcm.eq_1 div_zero dvd_zero gcd_dvd eq_div_of_mul_eq_right mul_assoc mul_right_comm
dvd_mod_iff 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instMod	—	dvd_add_right Dvd.dvd.mul_right div_add_mod
eq_div_iff_mul_eq_of_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	div_eq_iff_eq_mul_of_dvd
eq_div_of_mul_eq_left 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	instDiv	—	mul_div_cancel_right₀ toMulDivCancelClass
eq_div_of_mul_eq_right 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	instDiv	—	mul_div_cancel_left₀ toMulDivCancelClass
gcd_dvd 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing gcd	—	GCD.induction gcd_zero_left dvd_zero dvd_rfl gcd_val dvd_mod_iff
gcd_dvd_left 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing gcd	—	gcd_dvd
gcd_dvd_right 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing gcd	—	gcd_dvd
gcd_eq_gcd_ab 📖	mathematical	—	gcd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing Distrib.toMul gcdA gcdB	—	xgcdAux_P mul_one MulZeroClass.mul_zero add_zero zero_add xgcd_val xgcdAux_val
gcd_eq_left 📖	mathematical	—	gcd semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	—	gcd_dvd_right gcd_val mod_eq_zero gcd_zero_left
gcd_eq_zero_iff 📖	mathematical	—	gcd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	gcd_dvd gcd_zero_right
gcd_mul_lcm 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing gcd lcm	—	lcm.eq_1 MulZeroClass.zero_mul gcd_eq_zero_iff gcd_dvd mul_assoc mul_div_cancel_left₀ toMulDivCancelClass
gcd_one_left 📖	mathematical	—	gcd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toCommRing	—	gcd_eq_left one_dvd
gcd_self 📖	mathematical	—	gcd	—	gcd_eq_left dvd_rfl
gcd_val 📖	mathematical	—	gcd instMod	—	mod_lt gcd.eq_1 mod_zero gcd_zero_right
gcd_zero_right 📖	mathematical	—	gcd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	mod_lt gcd.eq_1 zero_mod gcd_zero_left
instIsDomain 📖	mathematical	—	IsDomain CommSemiring.toSemiring CommRing.toCommSemiring toCommRing	—	or_iff_not_and_not mul_div_cancel_right₀ toMulDivCancelClass zero_div NoZeroDivisors.to_isDomain toNontrivial IsDomain.toIsCancelMulZero
lcm_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	lcm	—	lcm.eq_1 div_zero gcd_eq_zero_iff gcd_dvd gcd_eq_gcd_ab mul_add Distrib.leftDistribClass dvd_add mul_left_comm mul_dvd_mul_left Dvd.dvd.mul_right mul_comm mul_div_cancel_left₀ toMulDivCancelClass mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain mul_assoc mul_right_comm
lcm_dvd_iff 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing lcm	—	Dvd.dvd.trans dvd_lcm_left dvd_lcm_right lcm_dvd
lcm_eq_zero_iff 📖	mathematical	—	lcm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	gcd_eq_zero_iff gcd_dvd mul_div_cancel_left₀ toMulDivCancelClass MulZeroClass.mul_zero mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain mul_div_assoc gcd_dvd_right lcm.eq_1 lcm_zero_left lcm_zero_right
lcm_zero_left 📖	mathematical	—	lcm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	lcm.eq_1 MulZeroClass.zero_mul zero_div
lcm_zero_right 📖	mathematical	—	lcm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	lcm.eq_1 MulZeroClass.mul_zero zero_div
mod_eq_sub_mul_div 📖	mathematical	—	instMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instDiv	—	add_sub_cancel_left div_add_mod
mod_eq_zero 📖	mathematical	—	instMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	div_add_mod add_zero dvd_mul_right add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd MulZeroClass.zero_mul mul_div_cancel_left₀ toMulDivCancelClass
mod_one 📖	mathematical	—	instMod AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mod_eq_zero one_dvd
mod_self 📖	mathematical	—	instMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	mod_eq_zero dvd_rfl
mul_add_div_left 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	—	eq_div_of_mul_eq_right mul_add Distrib.leftDistribClass mul_div_cancel'
mul_add_div_right 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul	—	mul_comm mul_add_div_left
mul_div_assoc 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	div_zero MulZeroClass.mul_zero mul_div_cancel_left₀ toMulDivCancelClass mul_left_comm
mul_div_cancel' 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instDiv	—	mul_div_assoc mul_div_cancel_left₀ toMulDivCancelClass
mul_div_mul_cancel 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	MulZeroClass.mul_zero div_zero eq_div_of_mul_eq_right mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain mul_assoc mul_div_assoc mul_dvd_mul_left mul_div_cancel_left₀ toMulDivCancelClass mul_ne_zero IsDomain.to_noZeroDivisors
mul_div_mul_comm_of_dvd_dvd 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	eq_or_ne MulZeroClass.zero_mul div_zero MulZeroClass.mul_zero mul_div_cancel_left₀ toMulDivCancelClass mul_mul_mul_comm mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain
mul_sub_div_left 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	eq_div_of_mul_eq_right mul_sub mul_div_cancel'
mul_sub_div_right 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	mul_comm mul_sub_div_left
sub_mul_div_left 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	eq_div_of_mul_eq_right mul_sub mul_div_cancel'
sub_mul_div_right 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	instDiv SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	mul_comm sub_mul_div_left
toMulDivCancelClass 📖	mathematical	—	MulDivCancelClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toCommRing instDiv	—	eq_of_sub_eq_zero mul_right_not_lt sub_eq_iff_eq_add' div_add_mod mul_comm sub_mul mod_lt
val_dvd_le 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing toCommRing	r	—	mul_left_not_lt MulZeroClass.mul_zero
xgcdAux_P 📖	mathematical	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing Distrib.toMul	xgcdAux	—	GCD.induction xgcd_zero_left mul_sub add_sub sub_add_eq_add_sub sub_sub mul_comm mul_assoc add_mul Distrib.rightDistribClass mod_eq_sub_mul_div
xgcdAux_fst 📖	mathematical	—	xgcdAux gcd	—	GCD.induction xgcd_zero_left gcd_zero_left gcd_val
xgcdAux_val 📖	mathematical	—	xgcdAux AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing gcd xgcd	—	xgcd.eq_1 xgcdAux_fst
zero_div 📖	mathematical	—	instDiv MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	by_cases div_zero MulZeroClass.zero_mul mul_div_cancel_right₀ toMulDivCancelClass
zero_mod 📖	mathematical	—	instMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	—	mod_eq_zero dvd_zero

---

← Back to Index