Unique factorization and normalization #
Main definitions #
UniqueFactorizationMonoid.normalizedFactors
: choose a multiset of prime factors that are unique by normalizing them.UniqueFactorizationMonoid.normalizationMonoid
: choose a way of normalizing the elements of a UFM
noncomputable def
UniqueFactorizationMonoid.normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
(a : α)
:
Multiset α
Noncomputably determines the multiset of prime factors.
Equations
Instances For
@[simp]
theorem
UniqueFactorizationMonoid.factors_eq_normalizedFactors
{M : Type u_2}
[CancelCommMonoidWithZero M]
[UniqueFactorizationMonoid M]
[Subsingleton Mˣ]
(x : M)
:
An arbitrary choice of factors of x : M
is exactly the (unique) normalized set of factors,
if M
has a trivial group of units.
theorem
UniqueFactorizationMonoid.prod_normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a : α}
(ane0 : a ≠ 0)
:
Associated (normalizedFactors a).prod a
@[deprecated UniqueFactorizationMonoid.prod_normalizedFactors (since := "2024-12-04")]
theorem
UniqueFactorizationMonoid.normalizedFactors_prod
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a : α}
(ane0 : a ≠ 0)
:
Associated (normalizedFactors a).prod a
theorem
UniqueFactorizationMonoid.prime_of_normalized_factor
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a : α}
(x : α)
:
x ∈ normalizedFactors a → Prime x
theorem
UniqueFactorizationMonoid.irreducible_of_normalized_factor
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a : α}
(x : α)
:
x ∈ normalizedFactors a → Irreducible x
theorem
UniqueFactorizationMonoid.normalize_normalized_factor
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a : α}
(x : α)
:
theorem
UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
(a p : α)
:
p ∈ normalizedFactors a → ∀ q ∈ normalizedFactors a, p ∣ q → p = q
theorem
UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a p : α}
(ha0 : a ≠ 0)
(hp : Irreducible p)
:
p ∣ a → ∃ q ∈ normalizedFactors a, Associated p q
theorem
UniqueFactorizationMonoid.exists_mem_normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{x : α}
(hx : x ≠ 0)
(h : ¬IsUnit x)
:
∃ (p : α), p ∈ normalizedFactors x
theorem
UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{x y : α}
(hx : x ≠ 0)
(hy : y ≠ 0)
:
theorem
UniqueFactorizationMonoid.zero_not_mem_normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
(x : α)
:
0 ∉ normalizedFactors x
theorem
UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a p : α}
(H : p ∈ normalizedFactors a)
:
theorem
UniqueFactorizationMonoid.mem_normalizedFactors_iff
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
[Subsingleton αˣ]
{p x : α}
(hx : x ≠ 0)
:
theorem
UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{p r : α}
(h : ∀ {m : α}, m ∈ normalizedFactors r → m = p)
(hr : r ≠ 0)
:
∃ (i : ℕ), Associated (p ^ i) r
theorem
UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
{a b c : α}
(ha : a ∈ normalizedFactors c)
(hb : b ∈ normalizedFactors c)
(h : Associated a b)
:
@[simp]
theorem
UniqueFactorizationMonoid.normalizedFactors_pos
{α : Type u_1}
[CancelCommMonoidWithZero α]
[NormalizationMonoid α]
[UniqueFactorizationMonoid α]
(x : α)
(hx : x ≠ 0)
:
noncomputable def
UniqueFactorizationMonoid.normalizationMonoid
{α : Type u_1}
[CancelCommMonoidWithZero α]
[UniqueFactorizationMonoid α]
:
Noncomputably defines a normalizationMonoid
structure on a UniqueFactorizationMonoid
.
Equations
- One or more equations did not get rendered due to their size.