lemma proved term proof

`phiRung_add`

show as: view Lean formalization →

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

generate prose now

formal statement (Lean)

 168lemma phiRung_add (m n : ℤ) : phiRung (m + n) = phiRung m * phiRung n := by

proof body

Term-mode proof.

 169  simp only [phiRung]
 170  exact zpow_add₀ phi_ne_zero m n
 171

depends on (6)

Lean names referenced from this declaration's body.

phi_ne_zero in IndisputableMonolith.Constants decl_use
phiRung in IndisputableMonolith.Constants.RSNativeUnits decl_use
phiRung in IndisputableMonolith.Gravity.UltramassiveBH decl_use
phi_ne_zero in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phiRung in IndisputableMonolith.NumberTheory.RecognitionTheta decl_use
phi_ne_zero in IndisputableMonolith.PhiSupport.Lemmas decl_use