theorem Factorization.associated_iff_exists_unit {R : Type u_1} [Monoid R] (a b : R) : Associated a b ↔ ∃ (u : Rˣ), a = b * ↑u

theorem Factorization.polynomial_irreducible_dvd_mul (F : Type u_1) [Field F] {p q s : Polynomial F} (hp : Irreducible p) (h : p ∣ q * s) : p ∣ q ∨ p ∣ s

theorem Factorization.gauss_lemma {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : (p * q).IsPrimitive

theorem Factorization.polynomial_ufd (R : Type u_1) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid (Polynomial R)

theorem Factorization.primitive_dvd_iff_fraction_map_dvd {R : Type u_1} [CommRing R] [IsDomain R] [Nonempty (NormalizedGCDMonoid R)] {p q : Polynomial R} (hp : p.IsPrimitive) : p ∣ q ↔ Polynomial.map (algebraMap R (FractionRing R)) p ∣ Polynomial.map (algebraMap R (FractionRing R)) q

theorem Factorization.gaussian_prime_of_norm_natAbs_prime (z : GaussianInt) (p : ℕ) (hpp : Nat.Prime p) (hn : (Zsqrtd.norm z).natAbs = p) : Prime z

theorem Factorization.gaussian_primes_classification : (∀ (p : ℕ) [Fact (Nat.Prime p)], Prime ↑p ↔ p % 4 = 3) ∧ (∀ (p : ℕ) [Fact (Nat.Prime p)], p % 4 = 1 → ∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p ∧ Prime { re := ↑a, im := ↑b } ∧ Prime { re := ↑a, im := -↑b }) ∧ Prime { re := 1, im := 1 } ∧ ∀ (z : GaussianInt), Prime z → (∃ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ∧ Associated z ↑p) ∨ (∃ (a : ℕ) (b : ℕ) (p : ℕ), Nat.Prime p ∧ p % 4 = 1 ∧ a ^ 2 + b ^ 2 = p ∧ (Associated z { re := ↑a, im := ↑b } ∨ Associated z { re := ↑a, im := -↑b })) ∨ Associated z { re := 1, im := 1 }

theorem Factorization.int_prime_not_gaussian_prime_iff (p : ℕ) [hp : Fact (Nat.Prime p)] : ¬Prime ↑↑p ↔ p = 2 ∨ p % 4 = 1

theorem Factorization.gaussian_not_prime_iff (p : ℕ) [hp : Fact (Nat.Prime p)] : ¬Prime ↑p ↔ p = 2 ∨ p % 4 = 1

theorem Factorization.fermat_last_theorem (n : ℕ) (hn : 2 < n) (a b c : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a ^ n + b ^ n ≠ c ^ n

theorem Factorization.ufd_gcd_exists {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (a b : R) : ∃ (g : R), g ∣ a ∧ g ∣ b ∧ ∀ (d : R), d ∣ a → d ∣ b → d ∣ g