theorem
proved
mod6_nineteen_prime
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 1864.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1861theorem mod6_thirteen_prime : Prime 13 ∧ 13 % 6 = 1 := by native_decide
1862
1863/-- 19 ≡ 1 (mod 6). -/
1864theorem mod6_nineteen_prime : Prime 19 ∧ 19 % 6 = 1 := by native_decide
1865
1866/-- 31 ≡ 1 (mod 6). -/
1867theorem mod6_thirtyone_prime : Prime 31 ∧ 31 % 6 = 1 := by native_decide
1868
1869/-- 37 ≡ 1 (mod 6) (RS-relevant). -/
1870theorem mod6_thirtyseven_prime : Prime 37 ∧ 37 % 6 = 1 := by native_decide
1871
1872/-- 43 ≡ 1 (mod 6). -/
1873theorem mod6_fortythree_prime : Prime 43 ∧ 43 % 6 = 1 := by native_decide
1874
1875/-- 61 ≡ 1 (mod 6). -/
1876theorem mod6_sixtyone_prime : Prime 61 ∧ 61 % 6 = 1 := by native_decide
1877
1878/-- 67 ≡ 1 (mod 6). -/
1879theorem mod6_sixtyseven_prime : Prime 67 ∧ 67 % 6 = 1 := by native_decide
1880
1881/-- 73 ≡ 1 (mod 6). -/
1882theorem mod6_seventythree_prime : Prime 73 ∧ 73 % 6 = 1 := by native_decide
1883
1884/-- 79 ≡ 1 (mod 6). -/
1885theorem mod6_seventynine_prime : Prime 79 ∧ 79 % 6 = 1 := by native_decide
1886
1887/-- 97 ≡ 1 (mod 6). -/
1888theorem mod6_ninetyseven_prime : Prime 97 ∧ 97 % 6 = 1 := by native_decide
1889
1890/-- 103 ≡ 1 (mod 6) (RS-relevant). -/
1891theorem mod6_onehundredthree_prime : Prime 103 ∧ 103 % 6 = 1 := by native_decide
1892
1893/-- 5 ≡ 5 (mod 6). -/
1894theorem mod6_five_prime : Prime 5 ∧ 5 % 6 = 5 := by native_decide