Radical of an element of a unique factorization normalization monoid

This file defines the radical of an element a in a unique factorization normalization monoid as the product of normalized prime factors of a without duplication. This is different from the radical of an ideal.

Lemmas relating to natural numbers and integers are in Mathlib.RingTheory.Radical.NatInt.

Main declarations

• radical: The radical of an element a in a unique factorization monoid is the product of its prime factors.
• radical_eq_of_associated: If a and b are associates, i.e. a * u = b for some unit u, then radical a = radical b.
• radical_mul_of_isUnit_left: Multiplying by a unit does not change the radical.
• radical_dvd_self: radical a divides a.
• radical_pow: radical (a ^ n) = radical a for any n ≥ 1.
• radical_of_prime: Radical of a prime element is equal to its normalization.
• radical_pow_of_prime: Radical of a power of a prime element is equal to its normalization.
• radical_mul, radical_prod: Radical is multiplicative for (pairwise) relatively prime elements.
• radical_mul_dvd, radical_prod_dvd: Radical of a product divides the product of radicals.

For Euclidean domains

• EuclideanDomain.divRadical: For an element a in a Euclidean domain, a / radical a.
• EuclideanDomain.divRadical_mul: divRadical of a product is the product of divRadicals.
• IsCoprime.divRadical: divRadical of coprime elements are coprime.

TODO

• Connect this notion with Ideal.radical. Particularly, for a principal ideal, Ideal.radical (Ideal.span {a}) = Ideal.span {radical a}.

noncomputable def UniqueFactorizationMonoid.primeFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) : Finset M

The finite set of prime factors of an element in a unique factorization monoid.

Equations

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

theorem UniqueFactorizationMonoid.mem_primeFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : a ∈ primeFactors b ↔ a ∈ normalizedFactors b

theorem Associated.primeFactors_eq {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : Associated a b) : UniqueFactorizationMonoid.primeFactors a = UniqueFactorizationMonoid.primeFactors b

@[simp]

theorem UniqueFactorizationMonoid.primeFactors_zero {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : primeFactors 0 = ∅

@[simp]

theorem UniqueFactorizationMonoid.primeFactors_one {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : primeFactors 1 = ∅

theorem UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : (↑(primeFactors a)).Pairwise IsRelPrime

theorem UniqueFactorizationMonoid.primeFactors_pow {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} (hn : n ≠ 0) : primeFactors (a ^ n) = primeFactors a

@[simp]

theorem UniqueFactorizationMonoid.primeFactors_pow' {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} [NeZero n] : primeFactors (a ^ n) = primeFactors a

theorem UniqueFactorizationMonoid.normalizedFactors_nodup {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : IsRadical a) : (normalizedFactors a).Nodup

theorem UniqueFactorizationMonoid.primeFactors_of_isUnit {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (h : IsUnit a) : primeFactors a = ∅

If x is a unit, then the finset of prime factors of x is empty. The converse is true with a nonzero assumption, see primeFactors_eq_empty_iff.

theorem UniqueFactorizationMonoid.primeFactors_eq_empty_iff {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : a ≠ 0) : primeFactors a = ∅ ↔ IsUnit a

The finset of prime factors of x is empty if and only if x is a unit. The converse is true without the nonzero assumption, see primeFactors_of_isUnit.

theorem UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : IsRadical a) : (primeFactors a).val = normalizedFactors a

theorem UniqueFactorizationMonoid.primeFactors_mul_eq_union {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} [DecidableEq M] (ha : a ≠ 0) (hb : b ≠ 0) : primeFactors (a * b) = primeFactors a ∪ primeFactors b

theorem UniqueFactorizationMonoid.disjoint_primeFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (hc : IsRelPrime a b) : Disjoint (primeFactors a) (primeFactors b)

Relatively prime elements have disjoint prime factors (as finsets).

theorem UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (hc : IsRelPrime a b) : primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

noncomputable def UniqueFactorizationMonoid.radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) : M

The radical of an element a in a unique factorization monoid is the product of the prime factors of a.

Equations

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

@[simp]

theorem UniqueFactorizationMonoid.radical_zero {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : radical 0 = 1

@[simp]

theorem UniqueFactorizationMonoid.radical_one {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : radical 1 = 1

theorem UniqueFactorizationMonoid.radical_eq_of_associated {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : Associated a b) : radical a = radical b

theorem UniqueFactorizationMonoid.radical_associated {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : IsRadical a) (ha' : a ≠ 0) : Associated (radical a) a

theorem IsRadical.dvd_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : IsRadical a) (ha' : a ≠ 0) : a ∣ UniqueFactorizationMonoid.radical a

If a is a radical element, then it divides its radical.

theorem UniqueFactorizationMonoid.radical_of_isUnit {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (h : IsUnit a) : radical a = 1

theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a u : M} (h : IsUnit u) : radical (u * a) = radical a

theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_right {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a u : M} (h : IsUnit u) : radical (a * u) = radical a

theorem UniqueFactorizationMonoid.radical_pow {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} (hn : n ≠ 0) : radical (a ^ n) = radical a

theorem UniqueFactorizationMonoid.radical_dvd_self {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : radical a ∣ a

theorem UniqueFactorizationMonoid.radical_of_prime {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : Prime a) : radical a = normalize a

theorem UniqueFactorizationMonoid.radical_pow_of_prime {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : Prime a) {n : ℕ} (hn : n ≠ 0) : radical (a ^ n) = normalize a

@[simp]

theorem UniqueFactorizationMonoid.radical_ne_zero {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} [Nontrivial M] : radical a ≠ 0

theorem UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (ha : Irreducible a) (hb : b ≠ 0) : a ∣ radical b ↔ a ∣ b

An irreducible a divides the radical of b if and only if it divides b itself. Note this generalises to radical elements a, see UniqueFactorizationMonoid.dvd_radical_iff.

theorem UniqueFactorizationMonoid.isRadical_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : IsRadical (radical a)

theorem UniqueFactorizationMonoid.squarefree_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : Squarefree (radical a)

@[simp]

theorem UniqueFactorizationMonoid.primeFactors_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : primeFactors (radical a) = primeFactors a

theorem UniqueFactorizationMonoid.radical_eq_iff_primeFactors_eq {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : radical a = radical b ↔ primeFactors a = primeFactors b

@[deprecated "This lemma is deprecated in favor of using `radical_eq_iff_primeFactors_eq.mpr`. " (since := "2025-11-09")]

theorem UniqueFactorizationMonoid.radical_eq_of_primeFactors_eq {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : primeFactors a = primeFactors b) : radical a = radical b

theorem UniqueFactorizationMonoid.radical_eq_one_iff {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : radical a = 1 ↔ a = 0 ∨ IsUnit a

@[simp]

theorem UniqueFactorizationMonoid.radical_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : radical (radical a) = radical a

theorem UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b

theorem UniqueFactorizationMonoid.radical_dvd_radical_iff_primeFactors_subset_primeFactors {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

theorem UniqueFactorizationMonoid.radical_dvd_radical {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : a ∣ b) (hb₀ : b ≠ 0) : radical a ∣ radical b

If a divides b, then the radical of a divides the radical of b. The theorem requires that b ≠ 0, since radical 0 = 1 but a ∣ 0 holds for every a.

theorem UniqueFactorizationMonoid.dvd_radical_iff {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (ha : IsRadical a) (hb₀ : b ≠ 0) : a ∣ radical b ↔ a ∣ b

If a is a radical element, then a divides the radical of b if and only if it divides b. Note the forward implication holds without the b ≠ 0 assumption via radical_dvd_self.

theorem UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (hb : b ≠ 0) : radical a ∣ b ↔ primeFactors a ⊆ primeFactors b

theorem UniqueFactorizationMonoid.radical_mul {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (hc : IsRelPrime a b) : radical (a * b) = radical a * radical b

Radical is multiplicative for relatively prime elements.

theorem UniqueFactorizationMonoid.radical_prod {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {ι : Type u_2} {f : ι → M} (s : Finset ι) (h : (↑s).Pairwise (Function.onFun IsRelPrime f)) : radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)

theorem UniqueFactorizationMonoid.radical_mul_dvd {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : radical (a * b) ∣ radical a * radical b

theorem UniqueFactorizationMonoid.radical_prod_dvd {M : Type u_1} [CommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {ι : Type u_2} {s : Finset ι} {f : ι → M} : radical (∏ i ∈ s, f i) ∣ ∏ i ∈ s, radical (f i)

Theorems for UFDs

@[simp]

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

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

noncomputable def EuclideanDomain.divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : E

Division of an element by its radical in a Euclidean domain.

Equations

• EuclideanDomain.divRadical a = a / UniqueFactorizationMonoid.radical a

theorem EuclideanDomain.radical_mul_divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a : E} : UniqueFactorizationMonoid.radical a * divRadical a = a

theorem EuclideanDomain.divRadical_mul_radical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a : E} : divRadical a * UniqueFactorizationMonoid.radical a = a

theorem EuclideanDomain.divRadical_ne_zero {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a : E} (ha : a ≠ 0) : divRadical a ≠ 0

theorem EuclideanDomain.divRadical_isUnit {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {u : E} (hu : IsUnit u) : IsUnit (divRadical u)

theorem EuclideanDomain.eq_divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a x : E} (h : UniqueFactorizationMonoid.radical a * x = a) : x = divRadical a

theorem EuclideanDomain.divRadical_mul {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a b : E} (hab : IsCoprime a b) : divRadical (a * b) = divRadical a * divRadical b

theorem EuclideanDomain.divRadical_dvd_self {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : divRadical a ∣ a

theorem IsCoprime.divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a b : E} (h : IsCoprime a b) : IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)