Repository navigation

Deduplicate redundant proofs: closed-range cokernel argument and diagonal-operator self-adjointness - #15

Merged

JonBannon merged 8 commits into

mainfrom

dedupe-redundancies

Jun 21, 2026

Commits on Jun 20, 2026

Sync blueprint with CompactOperators.lean and FourierHolomorphic.lean (M3a/M3b)

JonBannon
and
claude
committed
af31d03
Deduplicate the closed-range cokernel argument

JonBannon
and
claude
committed
0408535
Generalize the diagonal-operator domain/self-adjointness argument

JonBannon
and
claude
committed
1f4161e
Scope [DecidableEq alpha] to only where lp.single needs it

JonBannon
and
claude
committed
153854f
Eliminate the DecidableEq lint warnings properly

JonBannon
and
claude
committed
8c60310
Fix stale file:line references in FAITHFULNESS.md and add the new shared lemma

JonBannon
and
claude
committed
4b04356
Stop overclaiming the full Riesz-Schauder theorem for compact perturbations

JonBannon
and
claude
committed
9d0ad7e
Fix missing "and" between author names in the blueprint

JonBannon
and
claude
committed
8edaea5