Factors as finsupp

Main definitions

• UniqueFactorizationMonoid.factorization: the multiset of irreducible factors as a Finsupp.

noncomputable def factorization {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (n : α) : α →₀ ℕ

This returns the multiset of irreducible factors as a Finsupp.

Equations

• factorization n = Multiset.toFinsupp (UniqueFactorizationMonoid.normalizedFactors n)

theorem factorization_eq_count {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n p : α} : (factorization n) p = Multiset.count p (UniqueFactorizationMonoid.normalizedFactors n)

@[simp]

theorem factorization_zero {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] : factorization 0 = 0

@[simp]

theorem factorization_one {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] : factorization 1 = 0

@[simp]

theorem support_factorization {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n : α} : (factorization n).support = (UniqueFactorizationMonoid.normalizedFactors n).toFinset

The support of factorization n is exactly the Finset of normalized factors

@[simp]

theorem factorization_mul {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : factorization (a * b) = factorization a + factorization b

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

theorem factorization_pow {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {x : α} {n : ℕ} : factorization (x ^ n) = n • factorization x

For any p, the power of p in x^n is n times the power in x

theorem associated_of_factorization_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) (h : factorization a = factorization b) : Associated a b