Documentation

Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

The Moebius function on a unique factorization monoid #

We define the Moebius function on a unique factorization monoid.

Main definitions #

Main statements #

source
🔸 coverage
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
    Instances For
      source
      📐 coverage
      theorem Nat.moebius_eq (n : ℕ) :
      UniqueFactorizationMonoid.moebius n = ArithmeticFunction.moebius n
      source
      📐 coverage
      @[simp]
      theorem Squarefree.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Squarefree a) :
      UniqueFactorizationMonoid.moebius a = (-1) ^ (UniqueFactorizationMonoid.factors a).card
      source
      📐 coverage
      @[simp]
      theorem UniqueFactorizationMonoid.moebius_of_not_squarefree {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : ¬Squarefree a) :
      moebius a = 0
      source
      📐 coverage
      theorem UniqueFactorizationMonoid.moebius_zero {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] :
      moebius 0 = 0
      source
      📐 coverage
      theorem UniqueFactorizationMonoid.moebius_one {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] :
      moebius 1 = 1
      source
      📐 coverage
      theorem Associated.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) :
      UniqueFactorizationMonoid.moebius a = UniqueFactorizationMonoid.moebius b
      source
      📐 coverage
      theorem IsUnit.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : IsUnit a) :
      UniqueFactorizationMonoid.moebius a = 1
      source
      📐 coverage
      theorem Irreducible.moebius_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) :
      UniqueFactorizationMonoid.moebius a = -1
      source
      📐 coverage
      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