No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
1853theorem sigma_three_twelve : sigma 3 12 = 2044 := by native_decide
proof body
Term-mode proof.
1854
1855/-! ### Mod 6 prime classification (all primes > 3 are ≡ 1 or 5 mod 6) -/
1856
1857/-- 7 ≡ 1 (mod 6). -/
depends on (7)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
sigma
in IndisputableMonolith.Decision.AbileneParadox
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
sigma
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use