`lcm_eight_eighthundredforty`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 712 · 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 712.

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

 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
 728/-- σ_0(360) = 24. -/
 729theorem sigma_zero_threehundredsixty : sigma 0 360 = 24 := by native_decide
 730
 731/-- σ_1(8) = 15. -/
 732theorem sigma_one_eight : sigma 1 8 = 15 := by native_decide
 733
 734/-- σ_1(45) = 78. -/
 735theorem sigma_one_fortyfive : sigma 1 45 = 78 := by native_decide
 736
 737/-- σ_1(360) = 1170. -/
 738theorem sigma_one_threehundredsixty : sigma 1 360 = 1170 := by native_decide
 739
 740/-! ### Prime factors of primes and prime powers -/
 741
 742/-- The prime factors of a prime p is just {p}. -/

papers checked against this theorem

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