theorem proved term proof

`sigma_one_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)

 780theorem sigma_one_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 781    sigma 1 (m * n) = sigma 1 m * sigma 1 n :=

Term-mode proof.

 782  sigma_mul_of_coprime h
 783
 784/-! ### Totient product formula helpers -/
 785
 786/-- φ(n) > 0 for n > 0 (strengthened). -/

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