def OddPrimeOrFour (z : ℤ) : Prop

Being equal to 4 or odd.

Equations

• OddPrimeOrFour z = (z = 4 ∨ Prime z ∧ Odd z)

theorem OddPrimeOrFour.ne_zero {z : ℤ} (h : OddPrimeOrFour z) : z ≠ 0

theorem OddPrimeOrFour.ne_one {z : ℤ} (h : OddPrimeOrFour z) : z ≠ 1

theorem OddPrimeOrFour.one_lt_abs {z : ℤ} (h : OddPrimeOrFour z) : 1 < |z|

theorem OddPrimeOrFour.not_unit {z : ℤ} (h : OddPrimeOrFour z) : ¬IsUnit z

theorem OddPrimeOrFour.abs {z : ℤ} (h : OddPrimeOrFour z) : OddPrimeOrFour |z|

theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p

theorem associated_of_dvd {a : ℤ} {p : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (h : p ∣ a) : Associated p a

theorem dvd_or_dvd {a : ℤ} {p : ℤ} {x : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (hdvd : p ∣ a * x) : p ∣ a ∨ p ∣ x

theorem exists_associated_mem_of_dvd_prod'' {p : ℤ} (hp : OddPrimeOrFour p) {s : Multiset ℤ} (hs : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) (hdvd : p ∣ Multiset.prod s) : ∃ q, q ∈ s ∧ Associated p q

theorem factors_unique_prod' {f : Multiset ℤ} {g : Multiset ℤ} : (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) → (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g

noncomputable def oddFactors (x : ℤ) : Multiset ℤ

The odd factors.

Equations

• oddFactors x = Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)

theorem oddFactors.zero : oddFactors 0 = 0

theorem oddFactors.not_two_mem (x : ℤ) : ¬2 ∈ oddFactors x

theorem oddFactors.nonneg {z : ℤ} {a : ℤ} (ha : a ∈ oddFactors z) : 0 ≤ a

theorem oddFactors.pow (z : ℤ) (n : ℕ) : oddFactors (z ^ n) = n • oddFactors z

noncomputable def evenFactorExp (x : ℤ) : ℕ

The exponent of 2 in the factorization.

Equations

• evenFactorExp x = Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x)

theorem evenFactorExp.def (x : ℤ) : evenFactorExp x = Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x)

theorem evenFactorExp.zero : evenFactorExp 0 = 0

theorem evenFactorExp.pow (z : ℤ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z

theorem even_and_odd_factors'' (x : ℤ) : UniqueFactorizationMonoid.normalizedFactors x = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x

theorem even_and_odd_factors' (x : ℤ) : UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x

theorem even_and_oddFactors (x : ℤ) (hx : x ≠ 0) : Associated x (2 ^ evenFactorExp x * Multiset.prod (oddFactors x))

theorem factors_2_even {z : ℤ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z

noncomputable def factorsOddPrimeOrFour (z : ℤ) : Multiset ℤ

Odd factors or 4.

Equations

• factorsOddPrimeOrFour z = Multiset.replicate (evenFactorExp z / 2) 4 + oddFactors z

theorem factorsOddPrimeOrFour.nonneg {z : ℤ} {a : ℤ} (ha : a ∈ factorsOddPrimeOrFour z) : 0 ≤ a

theorem factorsOddPrimeOrFour.prod' {a : ℤ} (ha : 0 < a) (heven : Even (evenFactorExp a)) : Multiset.prod (factorsOddPrimeOrFour a) = a

theorem factorsOddPrimeOrFour.associated' {a : ℤ} {f : Multiset ℤ} (hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) (ha : 0 < a) (heven : Even (evenFactorExp a)) (hassoc : Associated (Multiset.prod f) a) : Multiset.Rel Associated f (factorsOddPrimeOrFour a)

theorem factorsOddPrimeOrFour.unique' {a : ℤ} {f : Multiset ℤ} (hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) (hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x) (ha : 0 < a) (heven : Even (evenFactorExp a)) (hassoc : Associated (Multiset.prod f) a) : f = factorsOddPrimeOrFour a

theorem factorsOddPrimeOrFour.pow (z : ℤ) (n : ℕ) (hz : Even (evenFactorExp z)) : factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z