theorem
proved
coprime_fortyfive_thirtyseven
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1070.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
1067theorem coprime_eight_thirtyseven : Nat.Coprime 8 37 := by native_decide
1068
1069/-- 45 and 37 are coprime. -/
1070theorem coprime_fortyfive_thirtyseven : Nat.Coprime 45 37 := by native_decide
1071
1072/-- gcd(360, 7) = 1 (7 does not divide 360). -/
1073theorem gcd_threehundredsixty_seven : Nat.gcd 360 7 = 1 := by native_decide
1074
1075/-- gcd(45, 8) = 1 (symmetric). -/
1076theorem gcd_fortyfive_eight : Nat.gcd 45 8 = 1 := by native_decide
1077
1078/-! ### More divisor counts -/
1079
1080/-- The number of divisors of 6 is 4. -/
1081theorem divisors_card_six : (6 : ℕ).divisors.card = 4 := by native_decide
1082
1083/-- The number of divisors of 10 is 4. -/
1084theorem divisors_card_ten : (10 : ℕ).divisors.card = 4 := by native_decide
1085
1086/-- The number of divisors of 12 is 6. -/
1087theorem divisors_card_twelve : (12 : ℕ).divisors.card = 6 := by native_decide
1088
1089/-- The number of divisors of 30 is 8. -/
1090theorem divisors_card_thirty : (30 : ℕ).divisors.card = 8 := by native_decide
1091
1092/-- The number of divisors of 60 is 12. -/
1093theorem divisors_card_sixty : (60 : ℕ).divisors.card = 12 := by native_decide
1094
1095/-- The number of divisors of 120 is 16. -/
1096theorem divisors_card_onehundredtwenty : (120 : ℕ).divisors.card = 16 := by native_decide
1097
1098/-! ### More Möbius values -/
1099
1100/-- μ(10) = 1 (squarefree with 2 prime factors). -/