∀ {n : ℕ} (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  (algebraMap (Polynomial R) (RatFunc R)) (Polynomial.cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal,
      (algebraMap (Polynomial R) (RatFunc R)) (Polynomial.X ^ i.2 - 1) ^ ArithmeticFunction.moebius i.1