Radical of an element of a unique factorization normalization monoid

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

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_unit_mul: Multiplying 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 prime element is equal to its normalization
• radical_mul: Radical is multiplicative for two relatively prime elements.
• radical_prod: Radical is multiplicative for finitely many relatively prime elements.

For unique factorization domains

For Euclidean domains

• EuclideanDomain.divRadical: For an element a in an 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.

For natural numbers

• UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors: The prime factors of a natural number are the same as the prime factors defined in Nat.primeFactors.
• Nat.radical_le_self: The radical of a natural number is less than or equal to the number itself.
• Nat.two_le_radical: If a natural number is at least 2, then its radical is at least 2.

TODO

• Make a comparison with Ideal.radical. Especially, for principal ideal, Ideal.radical (Ideal.span {a}) = Ideal.span {radical a}.

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

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

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

theorem Associated.primeFactors_eq {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : primeFactors 0 = ∅

@[simp]

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

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

theorem UniqueFactorizationMonoid.primeFactors_pow {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} [NeZero n] : primeFactors (a ^ n) = primeFactors a

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

theorem UniqueFactorizationMonoid.primeFactors_of_isUnit {M : Type u_1} [CancelCommMonoidWithZero 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 normalizedFactors_eq_zero_iff.

theorem UniqueFactorizationMonoid.primeFactors_eq_empty_iff {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (hc : IsRelPrime a b) : primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

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

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

@[simp]

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

@[deprecated UniqueFactorizationMonoid.radical_zero (since := "2025-05-31")]

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

Alias of UniqueFactorizationMonoid.radical_zero.

@[simp]

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

@[deprecated UniqueFactorizationMonoid.radical_one (since := "2025-05-31")]

theorem UniqueFactorizationMonoid.radical_one_eq {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : radical 1 = 1

Alias of UniqueFactorizationMonoid.radical_one.

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

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

theorem UniqueFactorizationMonoid.radical_associated {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (h : IsUnit a) : radical a = 1

theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a u : M} (h : IsUnit u) : radical (a * u) = radical a

theorem UniqueFactorizationMonoid.radical_pow {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : radical a ∣ a

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

theorem UniqueFactorizationMonoid.radical_pow_of_prime {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} [Nontrivial M] : radical a ≠ 0

theorem UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} : IsRadical (radical a)

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

@[simp]

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

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

@[simp]

theorem UniqueFactorizationMonoid.radical_radical {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} : radical (a * b) ∣ radical a * radical b

theorem UniqueFactorizationMonoid.radical_prod_dvd {M : Type u_1} [CancelCommMonoidWithZero 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

@[deprecated "UniqueFactorizationMonoid.disjoint_normalizedFactors, IsCoprime.isRelPrime" (since := "2025-05-31")]

theorem UniqueFactorizationDomain.disjoint_normalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : Disjoint (UniqueFactorizationMonoid.normalizedFactors a) (UniqueFactorizationMonoid.normalizedFactors b)

Coprime elements have disjoint prime factors (as multisets).

@[deprecated "UniqueFactorizationMonoid.disjoint_primeFactors, IsCoprime.isRelPrime" (since := "2025-05-31")]

theorem UniqueFactorizationDomain.disjoint_primeFactors {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : Disjoint (UniqueFactorizationMonoid.primeFactors a) (UniqueFactorizationMonoid.primeFactors b)

Coprime elements have disjoint prime factors (as finsets).

@[deprecated "UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion, IsCoprime.isRelPrime" (since := "2025-05-31")]

theorem UniqueFactorizationDomain.mul_primeFactors_disjUnion {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : UniqueFactorizationMonoid.primeFactors (a * b) = (UniqueFactorizationMonoid.primeFactors a).disjUnion (UniqueFactorizationMonoid.primeFactors b) ⋯

@[deprecated "UniqueFactorizationMonoid.radical_mul, IsCoprime.isRelPrime" (since := "2025-05-31")]

theorem UniqueFactorizationDomain.radical_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : UniqueFactorizationMonoid.radical (a * b) = UniqueFactorizationMonoid.radical a * UniqueFactorizationMonoid.radical b

Radical is multiplicative for coprime elements.

@[simp]

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

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

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

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

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)

theorem UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors : primeFactors = Nat.primeFactors

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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