theorem proved decidable or rfl

`JcostN_eq_Jcost_aggregate`

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

formal statement (Lean)

  51@[simp] theorem JcostN_eq_Jcost_aggregate {n : ℕ} (α x : Vec n) :
  52    JcostN α x = Jcost (aggregate α x) := by

Decided by rfl or decide.

  53  rfl
  54

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

JcostN_nonneg in IndisputableMonolith.Cost.Ndim.Core decl_use
forced_of_scalar_uniqueness in IndisputableMonolith.Cost.Ndim.Uniqueness decl_use

Lean names referenced from this declaration's body.