theorem proved term proof

`zero_eval`

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

formal statement (Lean)

  26theorem zero_eval (x : Fin 4 → ℝ) : eval zero x = 0 := rfl

Term-mode proof.

  27
  28/-- Scalar field addition. -/

Lean names referenced from this declaration's body.

eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use