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

involutionOp_diagOp_comm

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)

 171theorem involutionOp_diagOp_comm :
 172    involutionOp ∘ₗ diagOp = diagOp ∘ₗ involutionOp := by

proof body

Term-mode proof.

 173  ext v
 174  simp [costAt_neg_eq]
 175
 176/-- The reciprocal involution intertwines the prime-shift with its
 177    inverse: `U ∘ V_p = V_p^{-1} ∘ U`.
 178
 179    This is the operator-level analog of the zeta functional equation's
 180    involution `s ↔ 1-s`. -/

used by (2)

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

depends on (17)

Lean names referenced from this declaration's body.