theorem proved term proof

`costCompose_zero_left`

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

formal statement (Lean)

 136theorem costCompose_zero_left (a : ℝ) : (0 : ℝ) ★ a = 2 * a := by

Term-mode proof.

 137  unfold costCompose
 138  ring_nf
 139

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

costCompose_no_identity in IndisputableMonolith.Algebra.CostAlgebra decl_use

Lean names referenced from this declaration's body.