`gcd_eight_threehundredsixty`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 697 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 697.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

formal source

 694/-! ### Additional coprimality facts for RS constants -/
 695
 696/-- gcd(8, 360) = 8. -/
 697theorem gcd_eight_threehundredsixty : Nat.gcd 8 360 = 8 := by native_decide
 698
 699/-- gcd(45, 360) = 45. -/
 700theorem gcd_fortyfive_threehundredsixty : Nat.gcd 45 360 = 45 := by native_decide
 701
 702/-- gcd(8, 840) = 8. -/
 703theorem gcd_eight_eighthundredforty : Nat.gcd 8 840 = 8 := by native_decide
 704
 705/-- gcd(45, 840) = 15. -/
 706theorem gcd_fortyfive_eighthundredforty : Nat.gcd 45 840 = 15 := by native_decide
 707
 708/-- gcd(360, 840) = 120. -/
 709theorem gcd_threehundredsixty_eighthundredforty : Nat.gcd 360 840 = 120 := by native_decide
 710
 711/-- lcm(8, 840) = 840. -/
 712theorem lcm_eight_eighthundredforty : Nat.lcm 8 840 = 840 := by native_decide
 713
 714/-- lcm(45, 840) = 2520. -/
 715theorem lcm_fortyfive_eighthundredforty : Nat.lcm 45 840 = 2520 := by native_decide
 716
 717/-- lcm(360, 840) = 2520. -/
 718theorem lcm_threehundredsixty_eighthundredforty : Nat.lcm 360 840 = 2520 := by native_decide
 719
 720/-! ### Sigma values at RS constants -/
 721
 722/-- σ_0(8) = 4. -/
 723theorem sigma_zero_eight : sigma 0 8 = 4 := by native_decide
 724
 725/-- σ_0(45) = 6. -/
 726theorem sigma_zero_fortyfive : sigma 0 45 = 6 := by native_decide
 727

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.