extendedeuclidattempt

cymcymcymcym · Sep 27, 2024 · c85e6ad · c85e6ad
1 parent 1d43c6b
commit c85e6ad
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/UFT/UniquePrimeFactorization.lean b/UFT/UniquePrimeFactorization.lean
@@ -31,3 +31,5 @@ lemma prime_div_prime_implies_equality {α : Type} (R : WellOrderedRing α) (p :
     exact req
 
 --tbc
+ lemma extended_euclids_lemma {α : Type} (R : WellOrderedRing α) (p) (factor : List α) (hp : prime R p) (hfactor : ∀ q ∈ factor, prime R q) : p ∈ factor := by
+  sorry