From fc3d1d0f175b916e5abc036396067ad3e1a66909 Mon Sep 17 00:00:00 2001 From: matt Date: Sat, 21 Sep 2024 00:12:19 +0800 Subject: [PATCH] stuckatpower --- UFT/Axioms.lean | 116 +----------------- ...ion.lean => PrimeFactorizationExists.lean} | 7 -- UFT/PrimePowers.lean | 12 ++ UFT/UniquePrimeFactorization.lean | 31 +++++ 4 files changed, 44 insertions(+), 122 deletions(-) rename UFT/{PrimeFactorization.lean => PrimeFactorizationExists.lean} (95%) create mode 100644 UFT/PrimePowers.lean create mode 100644 UFT/UniquePrimeFactorization.lean diff --git a/UFT/Axioms.lean b/UFT/Axioms.lean index d21cf39..4078287 100644 --- a/UFT/Axioms.lean +++ b/UFT/Axioms.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Int.LeastGreatest +import Mathlib.Data.Set.Lattice structure myRing (α : Type) where add : α → α → α @@ -42,117 +42,3 @@ def myOrderedRing.ge {α : Type} (R : myOrderedRing α) (a b : α) : Prop := -- structure WellOrderedRing (α : Type) extends myOrderedRing α where well_ordered : ∀ (S : Set α), S.Nonempty → S ⊆ tomyOrderedRing.P → ∃ m ∈ S, ∀ s ∈ S, myOrderedRing.le tomyOrderedRing s m - --- Define the integer ring -def intRing : myRing Int :={ - add := Int.add, - mul := Int.mul, - zero := 0, - one := 1, - neg := Int.neg, - add_comm := Int.add_comm, - mul_comm := Int.mul_comm, - add_assoc := Int.add_assoc, - mul_assoc := Int.mul_assoc, - distrib := Int.mul_add, - add_zero := Int.add_zero, - add_inv := Int.add_right_neg, - mul_ident := Int.mul_one -} - -def intP : Set Int := - {x | x > 0} - -def orderedIntRing : myOrderedRing Int := { - tomyRing := intRing, - P := intP, - P_nonempty := ⟨1, by simp [intP]⟩, - P_add := by - intro a b ha hb - simp [intP] at * - exact Int.add_pos ha hb - - P_mul := by - intro a b ha hb - simp [intP] at * - exact Int.mul_pos ha hb - - trichotomy1 := by - simp [intP] - exact Int.zero_lt_one - - trichotomy2 := by - intro a ha - simp [intP] at * - have ha' : -a < 0 := by - exact Int.neg_neg_of_pos ha - exact Int.le_of_lt ha' - - trichotomy3 := by - intro a ha hza - simp [intP] at * - have hza' : 0 ≠ a := by - rw [ne_comm] - exact hza - have h : a < 0 := by - exact lt_of_le_of_ne' ha hza' - apply Int.neg_pos_of_neg - exact h -} - -def wellOrderedIntRing : WellOrderedRing Int := { - tomyOrderedRing := orderedIntRing, - well_ordered := by - intro S hS hP - - have Hinh : ∃ (z : ℤ), z ∈ S := by - exact hS - - have Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), z ∈ S → b ≤ z := ⟨0, by - intro z hz - have z_pos : z ∈ orderedIntRing.P := by - exact hP hz - have zero_le_pos : ∀ z ∈ orderedIntRing.P, 0 ≤ z := by - intro z' hzP - simp [intP] at hzP - exact Int.le_of_lt hzP - exact zero_le_pos z z_pos - ⟩ - - obtain ⟨lb, lb_in_S, is_least⟩ := Int.exists_least_of_bdd Hbdd Hinh - use lb - apply And.intro - · exact lb_in_S - - intro s s_in_S - unfold myOrderedRing.le - have Hle := is_least s s_in_S - by_cases h_eq : lb = s - · right - exact h_eq.symm - left - have Hlt : lb < s := by - exact lt_of_le_of_ne Hle h_eq - - have tmp : orderedIntRing.P = intP := by - rfl - rw [tmp] - simp [intP] - - have tmp2 : orderedIntRing.neg = Int.neg := by - rfl - rw [tmp2] - - have tmp3 : orderedIntRing.add = Int.add := by - rfl - rw [tmp3] - - simp - - have tmp4 : lb.neg = -lb := by - rfl - rw [tmp4] - - simp - exact Hlt -} diff --git a/UFT/PrimeFactorization.lean b/UFT/PrimeFactorizationExists.lean similarity index 95% rename from UFT/PrimeFactorization.lean rename to UFT/PrimeFactorizationExists.lean index bd88c5d..fa4e6ae 100644 --- a/UFT/PrimeFactorization.lean +++ b/UFT/PrimeFactorizationExists.lean @@ -13,13 +13,6 @@ def is_prime_factorization {α : Type} (R : WellOrderedRing α) (n : α) (factor (∀ p ∈ factors, prime R p) ∧ (list_product R factors = n) -def unique_prime_factorization {α : Type} (R : WellOrderedRing α) (n : α) : Prop := - ∀ (factors1 factors2 : List α), - is_prime_factorization R n factors1 → - is_prime_factorization R n factors2 → - ∃ (perm : List α → List α), - perm factors1 = factors2 - lemma prime_have_prime_factorization {α : Type} (R : WellOrderedRing α) (p : α) (pprime : prime R p) : is_prime_factorization R p [p] := by unfold is_prime_factorization constructor diff --git a/UFT/PrimePowers.lean b/UFT/PrimePowers.lean new file mode 100644 index 0000000..33fa067 --- /dev/null +++ b/UFT/PrimePowers.lean @@ -0,0 +1,12 @@ +import UFT.Axioms +import UFT.RingResults +import UFT.OrderedRingResults +import UFT.IntegralDomain +import UFT.Division +import UFT.GCD +import UFT.EuclidsLemma + +def power {α : Type} (R : WellOrderedRing α) (base : α) : α → α + | exp => + if exp = R.zero then R.one -- Base case: exponent is zero + else R.mul base (power R base (R.sub exp R.one)) -- Recursive case diff --git a/UFT/UniquePrimeFactorization.lean b/UFT/UniquePrimeFactorization.lean new file mode 100644 index 0000000..de899a9 --- /dev/null +++ b/UFT/UniquePrimeFactorization.lean @@ -0,0 +1,31 @@ +import UFT.Axioms +import UFT.RingResults +import UFT.OrderedRingResults +import UFT.IntegralDomain +import UFT.Division +import UFT.GCD +import UFT.EuclidsLemma +import UFT.PrimeFactorizationExists + +lemma prime_div_prime_implies_equality {α : Type} (R : WellOrderedRing α) (p : α) (q : α) + (hp : prime R p) (hq : prime R q) (hdiv : divisible R p q) : p = q := by + unfold prime at * + rcases hp with ⟨pgt1, pprime⟩ + rcases hq with ⟨qgt1, qprime⟩ + unfold divisible at hdiv + rcases hdiv with ⟨r, req⟩ + have p_gt0 := gt_transitive R.tomyOrderedRing p R.one R.zero pgt1 (one_gt_zero R.tomyOrderedRing) + have p_pos := gt0_implies_pos R.tomyOrderedRing p p_gt0 + have q_pos := gt0_implies_pos R.tomyOrderedRing q (gt_transitive R.tomyOrderedRing q R.one R.zero qgt1 (one_gt_zero R.tomyOrderedRing)) + have r_pos := pos_a_mul_b_eq_pos_c R.tomyOrderedRing p r q p_pos q_pos req + have r_gt0 := pos_implies_gt0 R.tomyOrderedRing r r_pos + have p1_or_r1 := qprime p r req p_gt0 r_gt0 + rcases p1_or_r1 with (p1 | r1) + · rw [p1] at pgt1 + unfold myOrderedRing.gt at pgt1 + rw [R.add_inv] at pgt1 + have zero_npos := R.trichotomy1 + contradiction + · rw [r1] at req + rw [R.mul_ident] at req + exact req