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

shiftInvOp_shiftOp

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)

 211theorem shiftInvOp_shiftOp (p : Nat.Primes) :
 212    shiftInvOp p ∘ₗ shiftOp p = LinearMap.id := by

proof body

Term-mode proof.

 213  ext v
 214  simp only [LinearMap.coe_comp, Function.comp_apply,
 215             shiftOp_single, shiftInvOp_single, Finsupp.lsingle_apply,
 216             LinearMap.id_apply]
 217  congr 1
 218  abel
 219
 220/-! ## The candidate Hilbert--Pólya operator (algebraic part) -/
 221
 222/-- The off-diagonal piece for a single prime: `V_p + V_p^{-1}`.
 223    This is the "hopping" term in the multiplicative direction `p`. -/

depends on (15)

Lean names referenced from this declaration's body.