theorem proved term proof

`costCompose_factored`

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

formal statement (Lean)

 156theorem costCompose_factored (a b : ℝ) :
 157    a ★ b = 2 * (a + 1) * (b + 1) - 2 := by

Term-mode proof.

 158  unfold costCompose; ring
 159
 160/-- The nonnegative `★`-magma has no identity element. -/

Lean names referenced from this declaration's body.