LeanPool.LeanPolyABC.Lib.Radical

noncomputable def LeanPolyABC.primeFactors {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) : Finset α

Prime factors of a are monic factors of a without duplication.

Equations

• LeanPolyABC.primeFactors a = (UniqueFactorizationMonoid.normalizedFactors a).toFinset

noncomputable def LeanPolyABC.radical {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) : α

Radical of a is a product of prime factors of a.

Equations

• LeanPolyABC.radical a = (LeanPolyABC.primeFactors a).prod id

theorem LeanPolyABC.radical_zero_eq_one {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : radical 0 = 1

theorem LeanPolyABC.radical_one_eq_one {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : radical 1 = 1

theorem LeanPolyABC.radical_associated_eq {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : radical a = radical b

theorem LeanPolyABC.radical_unit_eq_one {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (h : IsUnit a) : radical a = 1

theorem LeanPolyABC.radical_mul_unit_left {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {u a : α} (h : IsUnit u) : radical (u * a) = radical a

theorem LeanPolyABC.radical_mul_unit_right {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {u a : α} (h : IsUnit u) : radical (a * u) = radical a

theorem LeanPolyABC.primeFactors_pow {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) {n : ℕ} (hn : 0 < n) : primeFactors (a ^ n) = primeFactors a

theorem LeanPolyABC.radical_pow {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) {n : ℕ} (hn : 0 < n) : radical (a ^ n) = radical a

theorem LeanPolyABC.radical_dvd_self {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) : radical a ∣ a

theorem LeanPolyABC.radical_dvd_radical_self_mul {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (hb : b ≠ 0) : radical a ∣ radical (a * b)

theorem LeanPolyABC.radical_dvd_radical_mul_self {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (hb : b ≠ 0) : radical a ∣ radical (b * a)

theorem LeanPolyABC.radical_dvd_radical_of_dvd {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (hb : b ≠ 0) (h : a ∣ b) : radical a ∣ radical b

theorem LeanPolyABC.radical_mul_dvd_mul_radical {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a b : α) : radical (a * b) ∣ radical a * radical b

theorem LeanPolyABC.radical_prime {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Prime a) : radical a = normalize a

theorem LeanPolyABC.radical_prime_pow {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Prime a) {n : ℕ} (hn : 1 ≤ n) : radical (a ^ n) = normalize a

theorem LeanPolyABC.prime_dvd_radical_iff {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (ha : a ≠ 0) (hp : Prime p) : p ∣ radical a ↔ p ∣ a

theorem LeanPolyABC.radical_isUnit_iff {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (h : a ≠ 0) : IsUnit (radical a) ↔ IsUnit a

@[simp]

theorem LeanPolyABC.radical_neg_one {R : Type u_3} [CommRing R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] : radical (-1) = 1

theorem LeanPolyABC.radical_hMul {R : Type u_3} [CommRing R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : radical (a * b) = radical a * radical b

theorem LeanPolyABC.radical_neg {R : Type u_3} [CommRing R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a : R} : radical (-a) = radical a

theorem LeanPolyABC.radical_ne_zero {R : Type u_3} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] (a : R) : radical a ≠ 0

theorem LeanPolyABC.Polynomial.radical_degree_le {k : Type u_1} [Field k] [DecidableEq k] {a : Polynomial k} (ha : a ≠ 0) : (radical a).degree ≤ a.degree

theorem LeanPolyABC.Polynomial.radical_natDegree_le {k : Type u_1} [Field k] [DecidableEq k] (a : Polynomial k) : (radical a).natDegree ≤ a.natDegree

theorem LeanPolyABC.Polynomial.radical_natDegree_mul_le {k : Type u_1} [Field k] [DecidableEq k] (a b : Polynomial k) : (radical (a * b)).natDegree ≤ (radical a).natDegree + (radical b).natDegree