pith. machine review for the scientific record. sign in
theorem proved term proof

diagOp_single

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 126@[simp] theorem diagOp_single (v : MultIndex) (c : ℝ) :
 127    diagOp (Finsupp.single v c) = Finsupp.single v (costAt v * c) := by

proof body

Term-mode proof.

 128  simp [diagOp, mul_comm]
 129
 130/-- The prime-shift operator `V_p`: maps `e_v` to `e_{v + δ_p}`,
 131    i.e., multiplication of the underlying rational by `p`.
 132
 133    Defined via `Finsupp.lmapDomain` shifting the index by `δ_p`. -/

depends on (9)

Lean names referenced from this declaration's body.