The Moebius function on a unique factorization monoid

We define the Moebius function on a unique factorization monoid.

Main definitions

• UniqueFactorizationMonoid.moebius: The Moebius function on a unique factorization monoid, defined to be ((-1) ^ (factors a).card) if a is squarefree and 0 otherwise.

Main statements

• IsRelPrime.moebius_mul: The Moebius function is a multiplicative function.

noncomputable def UniqueFactorizationMonoid.moebius {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) : ℤ

The Moebius function on a unique factorization monoid, defined to be ((-1) ^ (factors a).card) if a is squarefree and 0 otherwise.

Equations

• UniqueFactorizationMonoid.moebius a = if Squarefree a then (-1) ^ (UniqueFactorizationMonoid.factors a).card else 0

theorem Nat.moebius_eq (n : ℕ) : UniqueFactorizationMonoid.moebius n = ArithmeticFunction.moebius n

@[simp]

theorem Squarefree.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Squarefree a) : UniqueFactorizationMonoid.moebius a = (-1) ^ (UniqueFactorizationMonoid.factors a).card

@[simp]

theorem UniqueFactorizationMonoid.moebius_of_not_squarefree {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : ¬Squarefree a) : moebius a = 0

theorem UniqueFactorizationMonoid.moebius_zero {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] : moebius 0 = 0

theorem UniqueFactorizationMonoid.moebius_one {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : moebius 1 = 1

theorem Associated.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : UniqueFactorizationMonoid.moebius a = UniqueFactorizationMonoid.moebius b

theorem IsUnit.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : IsUnit a) : UniqueFactorizationMonoid.moebius a = 1

theorem Irreducible.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : UniqueFactorizationMonoid.moebius a = -1

theorem IsRelPrime.moebius_mul {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : IsRelPrime a b) : UniqueFactorizationMonoid.moebius (a * b) = UniqueFactorizationMonoid.moebius a * UniqueFactorizationMonoid.moebius b