The radical in ℕ and ℤ

Declarations for ℕ

• UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors: The prime factors of a natural number are the same as the prime factors defined in Nat.primeFactors.
• Nat.radical_eq_prod_primeFactors: The radical is computable for natural numbers.
• Nat.radical_le_self_iff: if n ≠ 0, radical n ≤ n.
• Nat.two_le_radical_iff: 2 ≤ n.radical iff 2 ≤ n.

Declarations for ℤ

• UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs: The prime factors of an integer are the same as the prime factors of its absolute value.
• Int.radical_eq_prod_primeFactors: The radical is computable for integers.

Lemmas about natural numbers

theorem UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors : primeFactors = Nat.primeFactors

theorem Nat.radical_eq_prod_primeFactors {n : ℕ} : UniqueFactorizationMonoid.radical n = ∏ p ∈ n.primeFactors, p

theorem Nat.radical_pos (n : ℕ) : 0 < UniqueFactorizationMonoid.radical n

@[simp]

theorem Nat.one_lt_radical_iff {n : ℕ} : 1 < UniqueFactorizationMonoid.radical n ↔ 1 < n

@[simp]

theorem Nat.two_le_radical_iff {n : ℕ} : 2 ≤ UniqueFactorizationMonoid.radical n ↔ 2 ≤ n

@[simp]

theorem Nat.radical_le_one_iff {n : ℕ} : UniqueFactorizationMonoid.radical n ≤ 1 ↔ n ≤ 1

@[simp]

theorem Nat.radical_eq_one_iff {n : ℕ} : UniqueFactorizationMonoid.radical n = 1 ↔ n ≤ 1

@[simp]

theorem Nat.radical_le_self_iff {n : ℕ} : UniqueFactorizationMonoid.radical n ≤ n ↔ n ≠ 0

@[simp]

theorem Nat.self_lt_radical_iff {n : ℕ} : n < UniqueFactorizationMonoid.radical n ↔ n = 0

def Nat.Mathlib.Meta.Positivity.evalRadical : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for radical. Proves radicals are nonzero.

Lemmas about integers

theorem UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs {z : ℤ} : primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

@[simp]

theorem Int.radical_natAbs_eq_radical {z : ℤ} : ↑(UniqueFactorizationMonoid.radical z.natAbs) = UniqueFactorizationMonoid.radical z

theorem Int.radical_eq_prod_primeFactors {z : ℤ} : UniqueFactorizationMonoid.radical z = ↑(∏ p ∈ z.natAbs.primeFactors, p)

theorem Int.radical_pos (z : ℤ) : 0 < UniqueFactorizationMonoid.radical z

@[simp]

theorem Int.one_lt_radical_iff {z : ℤ} : 1 < UniqueFactorizationMonoid.radical z ↔ 1 < z.natAbs

@[simp]

theorem Int.two_le_radical_iff {z : ℤ} : 2 ≤ UniqueFactorizationMonoid.radical z ↔ 2 ≤ z.natAbs

@[simp]

theorem Int.radical_le_one_iff {z : ℤ} : UniqueFactorizationMonoid.radical z ≤ 1 ↔ z.natAbs ≤ 1

@[simp]

theorem Int.radical_eq_one_iff {z : ℤ} : UniqueFactorizationMonoid.radical z = 1 ↔ z.natAbs ≤ 1