card_finMulAntidiag_of_squarefree

English

If n is squarefree, the cardinality of finMulAntidiag d n equals d raised to the ω(n), i.e., the number of distinct prime factors of n.

Русский

Если n квадратно-безкратно, кардинальность finMulAntidiag d n равна d^{ω(n)}.

LaTeX

$$$\#(\text{finMulAntidiag}\ d\ n) = d^{\omega(n)}$$$

Lean4

theorem card_finMulAntidiag_of_squarefree {d n : ℕ} (hn : Squarefree n) : #(finMulAntidiag d n) = d ^ ω n := by
  rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const, ArithmeticFunction.cardDistinctFactors_apply,
    ← List.card_toFinset, toFinset_factors, Finset.card_fin]

Похожие утверждения