theorem
proved
six_almost_prime_threehundredsixty
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 2709.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2706theorem six_almost_prime_threehundredfiftytwo : isSixAlmostPrime 352 = true := by native_decide
2707
2708/-- 360 = 2³ × 3² × 5 is 6-almost prime (RS-relevant: main superperiod). -/
2709theorem six_almost_prime_threehundredsixty : isSixAlmostPrime 360 = true := by native_decide
2710
2711-- Note: 384 = 2⁷ × 3, Ω = 7 + 1 = 8, so not 6-almost prime.
2712
2713/-- 400 = 2⁴ × 5² is 6-almost prime. -/
2714theorem six_almost_prime_fourhundred : isSixAlmostPrime 400 = true := by native_decide
2715
2716/-- 416 = 2⁵ × 13 is 6-almost prime. -/
2717theorem six_almost_prime_fourhundredsixteen : isSixAlmostPrime 416 = true := by native_decide
2718
2719-- Note: 432 = 2⁴ × 3³, Ω = 4 + 3 = 7, so not 6-almost prime.
2720
2721-- Note: 448 = 2⁶ × 7, Ω = 6 + 1 = 7, so not 6-almost prime.
2722
2723/-- 486 = 2 × 3⁵ is 6-almost prime. -/
2724theorem six_almost_prime_fourhundredeightysix : isSixAlmostPrime 486 = true := by native_decide
2725
2726-- Note: 500 = 2² × 5³, Ω = 2 + 3 = 5, so not 6-almost prime.
2727
2728/-- 528 = 2⁴ × 3 × 11 is 6-almost prime (RS-relevant: 11). -/
2729theorem six_almost_prime_fivehundredtwentyeight : isSixAlmostPrime 528 = true := by native_decide
2730
2731/-- 544 = 2⁵ × 17 is 6-almost prime (RS-relevant: 17). -/
2732theorem six_almost_prime_fivehundredfortyfour : isSixAlmostPrime 544 = true := by native_decide
2733
2734/-- 560 = 2⁴ × 5 × 7 is 6-almost prime. -/
2735theorem six_almost_prime_fivehundredsixty : isSixAlmostPrime 560 = true := by native_decide
2736
2737-- Note: 576 = 2⁶ × 3², Ω = 6 + 2 = 8, so not 6-almost prime.
2738
2739/-- 624 = 2⁴ × 3 × 13 is 6-almost prime. -/