theorem proved term proof

`phi_power_compose`

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

formal statement (Lean)

 271theorem phi_power_compose (a b : ℤ) :
 272    PhiForcing.φ ^ a * PhiForcing.φ ^ b = PhiForcing.φ ^ (a + b) :=

Term-mode proof.

 273  (zpow_add₀ PhiForcing.phi_pos.ne' a b).symm
 274

From the project-wide theorem graph. These declarations reference this one in their body.

ladder_cascade_bound in IndisputableMonolith.Foundation.StillnessGenerative decl_use