SinTan1729/lean-talk-sp24
1
0
Fork 0
mirror of https://github.com/SinTan1729/lean-talk-sp24.git synced 2024-12-26 05:38:37 -06:00
Code Issues Projects Releases Packages Wiki Activity

chg: Broken some steps for easier understanding

Browse source
This commit is contained in:
Sayantan Santra 2024-02-06 01:35:56 -06:00
parent 5b38350326
commit a7bde3532c
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
LeanTalkSP24/infinitely_many_primes.lean
View file

@ -23,13 +23,15 @@ theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p
have : m ≠ 0 := by have : m ≠ 0 := by
intro mz intro mz
rw [mz, zero_dvd_iff] at mdvdn rw [mz, zero_dvd_iff] at mdvdn
linarith -- linarith
rw [mz, mdvdn] at mltn
contradiction
have mgt2 : 2 ≤ m := two_le this mne1 have mgt2 : 2 ≤ m := two_le this mne1
by_cases mp : m.Prime by_cases mp : m.Prime
· use m, mp · use m, mp
. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩ . rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
use p, pp use p, pp
apply pdvd.trans mdvdn exact Nat.dvd_trans pdvd mdvdn
theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
intro n intro n