Basic

📁 Source: Mathlib/Data/Nat/GCD/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `dvd_mul_left`, `dvd_mul_right`, `eq_of_mul_eq_zero`, `lcm_eq_mul`, `mul_add_mul_ne_mul`, `of_dvd`, `of_dvd_left`, `of_dvd_right`, `symmetric`, `nat_lcm_left`, `nat_lcm_right`, `add_coprime_iff_left`, `add_coprime_iff_right`, `coprime_add_iff_left`, `coprime_add_iff_right`, `coprime_add_mul_left_left`, `coprime_add_mul_left_right`, `coprime_add_mul_right_left`, `coprime_add_mul_right_right`, `coprime_add_self_left`, `coprime_add_self_right`, `coprime_iff_isRelPrime`, `coprime_mul_left_add_left`, `coprime_mul_left_add_right`, `coprime_mul_right_add_left`, `coprime_mul_right_add_right`, `coprime_one_left_iff`, `coprime_one_right_iff`, `coprime_pow_left_iff`, `coprime_pow_right_iff`, `coprime_self_add_left`, `coprime_self_add_right`, `coprime_self_sub_left`, `coprime_self_sub_right`, `coprime_sub_self_left`, `coprime_sub_self_right`, `div_dvd_div_left`, `div_lcm_eq_div_gcd`, `div_mul_div`, `dvd_lcm_of_dvd_left`, `dvd_lcm_of_dvd_right`, `dvd_of_lcm_left_dvd`, `dvd_of_lcm_right_dvd`, `eq_one_of_dvd_coprimes`, `gcd_greatest`, `gcd_mul_gcd_eq_iff_dvd_mul_of_coprime`, `gcd_mul_of_coprime_of_dvd`, `not_coprime_zero_zero`, `pow_sub_one_gcd_pow_sub_one`, `pow_sub_one_mod_pow_sub_one`	50
Total	50

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_coprime_iff_left` 📖	—	—	—	—	—
`add_coprime_iff_right` 📖	—	—	—	—	—
`coprime_add_iff_left` 📖	—	—	—	—	—
`coprime_add_iff_right` 📖	—	—	—	—	—
`coprime_add_mul_left_left` 📖	—	—	—	—	—
`coprime_add_mul_left_right` 📖	—	—	—	—	—
`coprime_add_mul_right_left` 📖	—	—	—	—	—
`coprime_add_mul_right_right` 📖	—	—	—	—	—
`coprime_add_self_left` 📖	—	—	—	—	—
`coprime_add_self_right` 📖	—	—	—	—	—
`coprime_iff_isRelPrime` 📖	mathematical	—	`IsRelPrime` `instMonoid`	—	`dvd_rfl`
`coprime_mul_left_add_left` 📖	—	—	—	—	—
`coprime_mul_left_add_right` 📖	—	—	—	—	—
`coprime_mul_right_add_left` 📖	—	—	—	—	—
`coprime_mul_right_add_right` 📖	—	—	—	—	—
`coprime_one_left_iff` 📖	—	—	—	—	—
`coprime_one_right_iff` 📖	—	—	—	—	—
`coprime_pow_left_iff` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	—
`coprime_pow_right_iff` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`coprime_pow_left_iff`
`coprime_self_add_left` 📖	—	—	—	—	—
`coprime_self_add_right` 📖	—	—	—	—	`add_comm` `coprime_add_self_right`
`coprime_self_sub_left` 📖	—	—	—	—	—
`coprime_self_sub_right` 📖	—	—	—	—	—
`coprime_sub_self_left` 📖	—	—	—	—	—
`coprime_sub_self_right` 📖	—	—	—	—	—
`div_dvd_div_left` 📖	—	—	—	—	`div_mul_div`
`div_lcm_eq_div_gcd` 📖	—	—	—	—	`div_dvd_div_left`
`div_mul_div` 📖	—	—	—	—	`MulZeroClass.mul_zero` `mul_assoc`
`dvd_lcm_of_dvd_left` 📖	—	—	—	—	`Dvd.dvd.trans`
`dvd_lcm_of_dvd_right` 📖	—	—	—	—	`Dvd.dvd.trans`
`dvd_of_lcm_left_dvd` 📖	—	—	—	—	`Dvd.dvd.trans`
`dvd_of_lcm_right_dvd` 📖	—	—	—	—	`Dvd.dvd.trans`
`eq_one_of_dvd_coprimes` 📖	—	—	—	—	`isUnit_iff_dvd_one` `coprime_iff_isRelPrime`
`gcd_greatest` 📖	—	—	—	—	`dvd_antisymm` `instIsCancelMulZero` `Unique.instSubsingleton`
`gcd_mul_gcd_eq_iff_dvd_mul_of_coprime` 📖	—	—	—	—	`dvd_antisymm` `instIsCancelMulZero` `Unique.instSubsingleton`
`gcd_mul_of_coprime_of_dvd` 📖	—	—	—	—	`exists_eq_mul_left_of_dvd` `one_mul`
`not_coprime_zero_zero` 📖	—	—	—	—	—
`pow_sub_one_gcd_pow_sub_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	—
`pow_sub_one_mod_pow_sub_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`zero_pow_eq` `zero_add` `one_pow` `pow_zero` `lt_or_ge` `pow_add` `MulZeroClass.mul_zero`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_mul_left` 📖	—	—	—	—	`dvd_mul_of_dvd_right`
`dvd_mul_right` 📖	—	—	—	—	`dvd_mul_of_dvd_left`
`eq_of_mul_eq_zero` 📖	—	—	—	—	—
`lcm_eq_mul` 📖	—	—	—	—	`one_mul`
`mul_add_mul_ne_mul` 📖	—	—	—	—	`mul_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `mul_ne_zero_iff` `mul_comm` `eq_zero_of_mul_eq_self_left` `mul_assoc`
`of_dvd` 📖	—	—	—	—	`of_dvd_right` `of_dvd_left`
`of_dvd_left` 📖	—	—	—	—	—
`of_dvd_right` 📖	—	—	—	—	—
`symmetric` 📖	mathematical	—	`Symmetric`	—	—

Nat.Dvd.dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nat_lcm_left` 📖	—	—	—	—	`Nat.dvd_lcm_of_dvd_right`
`nat_lcm_right` 📖	—	—	—	—	`Nat.dvd_lcm_of_dvd_left`

---

← Back to Index