theorem proved term proof

`sigma_zero_mul_of_coprime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 775theorem sigma_zero_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 776    sigma 0 (m * n) = sigma 0 m * sigma 0 n :=

Term-mode proof.

 777  sigma_mul_of_coprime h
 778
 779/-- σ_1(mn) = σ_1(m) × σ_1(n) for coprime m, n. -/

Lean names referenced from this declaration's body.

sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
sigma in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
sigma_mul_of_coprime in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use